:: HENMODEL semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

{} is set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

k is non empty finite Element of bool NAT
[:Al,k:] is finite set
bool [:Al,k:] is non empty finite V43() set

rng P is finite Element of bool k
bool k is non empty finite V43() set
dom P is finite Element of bool Al
bool Al is non empty finite V43() set
P . (union Al) is set
union (rng P) is set
ll is set

P . CX is set
ll is set
CX is set
JH is set
P . JH is set

P . rel is set
P . fin9 is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not fin9 <= b1 } is set

Al is non empty finite Element of bool NAT
union Al is set

dom P is set
field (RelIncl Al) is finite set
ll is set
rng P is set
field () is set
P . ll is set

dom CX is set

CX . JH is set

CX . rel is set
rng CX is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not JH <= b1 } is set
[rel,JH] is V26() Element of
is non empty non trivial non finite set
{rel,JH} is finite V43() set
{rel} is non empty trivial finite V43() 1 -element set
{{rel,JH},{rel}} is finite V43() set
[(CX . rel),(CX . JH)] is V26() set
{(CX . rel),(CX . JH)} is finite set
{(CX . rel)} is non empty trivial finite 1 -element set
{{(CX . rel),(CX . JH)},{(CX . rel)}} is finite V43() set

field (RelIncl JH) is finite set

rng CX is set
[:JH,Al:] is finite set
bool [:JH,Al:] is non empty finite V43() set

dom rel is finite Element of bool JH
bool JH is non empty finite V43() set

rel . fin9 is set
rel . a is set
rng rel is finite Element of bool Al
bool Al is non empty finite V43() set

rel . (union JH) is set
union (rng rel) is set

fin9 is set
a is set
rel . a is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not rel <= b1 } is set

Al is non empty set
[:NAT,Al:] is non empty non trivial non finite set
bool [:NAT,Al:] is non empty non trivial non finite set

dom k is Element of bool NAT
rng k is Element of bool Al
bool Al is non empty set
union (rng k) is set
P is finite set
{ } is set
min* { } is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT

dom ll is set
rng ll is set
JH is set
CX is finite set
rel is set
ll . rel is set
{ } is set
min* { } is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is set
JH is non empty finite Element of bool NAT
union JH is set

k . rel is Element of Al
fin9 is set
a is set
i is set
k . i is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : fin9 in k . b1 } is set
F is set
F is non empty set

k . F is Element of Al
ll . fin9 is set
F is non empty Element of bool NAT

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not rel <= b1 } is set
k . F is Element of Al

k . F is Element of Al

k . F is Element of Al

k . ll is Element of Al

k . CX is Element of Al

k . JH is Element of Al
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)

rng P is finite Element of bool (CQC-WFF Al)
ll is Element of CQC-WFF Al

'not' ll is Element of CQC-WFF Al

Al is non empty Relation-like QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
k is Element of CQC-WFF Al

Suc ((P ^ ll) ^ <*k*>) is Element of CQC-WFF Al
Suc (P ^ <*k*>) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

CX is Element of CQC-WFF Al

rng JH is finite Element of bool (CQC-WFF Al)

rng rel is finite Element of bool (CQC-WFF Al)

(rng JH) \/ (rng ll) is finite Element of bool (CQC-WFF Al)

VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al

rng ll is finite Element of bool (CQC-WFF Al)

rng CX is finite Element of bool (CQC-WFF Al)

rng (ll ^ CX) is finite Element of bool (CQC-WFF Al)
JH is Element of bool (CQC-WFF Al)
(rng ll) \/ (rng CX) is finite Element of bool (CQC-WFF Al)

Seg (len (Al ^ k)) is finite len (Al ^ k) -element Element of bool NAT

Seg (len Al) is finite len Al -element Element of bool NAT

seq ((len Al),(len k)) is Element of bool NAT
(Seg (len Al)) \/ (seq ((len Al),(len k))) is Element of bool NAT
dom (Al ^ k) is finite Element of bool NAT
dom Al is finite Element of bool NAT
(dom Al) \/ (seq ((len Al),(len k))) is Element of bool NAT
Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {P} is Element of bool (CQC-WFF Al)

ll is Element of CQC-WFF Al

rng CX is finite Element of bool (CQC-WFF Al)

CX " {P} is finite Element of bool NAT
dom CX is finite Element of bool NAT
rel is finite set

Seg (card rel) is finite card rel -element Element of bool NAT
K253((Seg (card rel)),P) is Relation-like Seg (card rel) -defined {P} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card rel)),{P}:]
{P} is non empty trivial finite 1 -element set
[:(Seg (card rel)),{P}:] is finite set
bool [:(Seg (card rel)),{P}:] is non empty finite V43() set

rel is finite set

Seg (len CX) is finite len CX -element Element of bool NAT

i - (len (CX - {P})) is ext-real V32() V37() integer set
seq ((len (CX - {P})),(card rel)) is Element of bool NAT

C is ext-real V32() V37() integer set

dom (Sgm rel) is finite Element of bool NAT
i is set

CX . C is set
rel \ rel is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (CX - {P})) is finite len (CX - {P}) -element Element of bool NAT

F is finite set

(card rel) - (card rel) is ext-real V32() V37() integer set

(card (Seg (len CX))) - (card rel) is ext-real V32() V37() integer set
(len CX) - (card rel) is ext-real V32() V37() integer set
len ((CX - {P}) ^ (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((CX - {P}) ^ (IdFinS (P,(card rel))))) is finite len ((CX - {P}) ^ (IdFinS (P,(card rel)))) -element Element of bool NAT

(Sgm (rel \ rel)) . F is set
F - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (F - (len (CX - {P}))) is set
F is set
F is set

F is set

dom (Sgm F) is finite Element of bool NAT

rng F is finite set
F is set

F . F is set
(Sgm F) . F is set
rng (Sgm F) is finite Element of bool NAT
rng (Sgm rel) is finite Element of bool NAT
F - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (F - (len (CX - {P}))) is set
(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT
F is set
F is set

(Sgm F) . F is set

F . F is set

(Sgm rel) . F is set

(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT
(j + (len (CX - {P}))) - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . ((j + (len (CX - {P}))) - (len (CX - {P}))) is set
F . (j + (len (CX - {P}))) is set
(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len CX) - (card rel)) + (len (IdFinS (P,(card rel)))) is ext-real V32() V37() integer set
((len CX) - (card rel)) + (card rel) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel

j is set
dom F is finite set
F . j is set
h is set
F . h is set
dom F is finite Element of bool rel
(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT
(Sgm F) . j is set
rng (Sgm F) is finite Element of bool NAT

k - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (k - (len (CX - {P}))) is set
rng (Sgm rel) is finite Element of bool NAT
(Sgm F) . h is set

k - (len (CX - {P})) is ext-real V32() V37() integer set

g - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (g - (len (CX - {P}))) is set
(Sgm rel) . (k - (len (CX - {P}))) is set
(g - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set
(k - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set
[:(dom CX),(dom CX):] is finite set
bool [:(dom CX),(dom CX):] is non empty finite V43() set

dom j is finite Element of bool (dom CX)
bool (dom CX) is non empty finite V43() set

j . h is set

dom (Per (CX,j)) is finite Element of bool NAT
dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT

j * CX is Relation-like dom CX -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom CX),(CQC-WFF Al):]
[:(dom CX),(CQC-WFF Al):] is set
bool [:(dom CX),(CQC-WFF Al):] is non empty set
dom (j * CX) is finite Element of bool (dom CX)
dom (IdFinS (P,(card rel))) is finite card rel -element Element of bool NAT

j . k is set
k - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (k - (len (CX - {P}))) is set
rng (Sgm rel) is finite Element of bool NAT
CX . (j . k) is set
(j * CX) . k is set
(Per (CX,j)) . k is set
(IdFinS (P,(card rel))) . g is set
((CX - {P}) ^ (IdFinS (P,(card rel)))) . k is set
dom (CX - {P}) is finite Element of bool NAT
(Sgm F) . k is set
CX . ((Sgm F) . k) is set

[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
((Sgm F) * CX) . k is set
(CX - {P}) . k is set
(j * CX) . h is set

k . h is set
(CX - {P}) . h is set
rng (CX - {P}) is finite set
(rng CX) \ {P} is finite Element of bool (CQC-WFF Al)

rng g is finite Element of bool (CQC-WFF Al)
(k \/ {P}) \ {P} is Element of bool (CQC-WFF Al)
k \ {P} is Element of bool (CQC-WFF Al)

rng rel is finite Element of bool (CQC-WFF Al)

rng fin9 is finite Element of bool (CQC-WFF Al)

Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
{()} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {()} is Element of bool (CQC-WFF Al)

rng ll is finite Element of bool (CQC-WFF Al)

dom <*()*> is non empty trivial finite 1 -element Element of bool NAT

dom (Ant ((ll ^ <*()*>) ^ <*()*>)) is finite Element of bool NAT
Suc ((ll ^ <*()*>) ^ <*()*>) is Element of CQC-WFF Al
(Ant ((ll ^ <*()*>) ^ <*()*>)) . ((len ll) + 1) is set

Suc (ll ^ <*()*>) is Element of CQC-WFF Al
rng (ll ^ <*()*>) is finite Element of bool (CQC-WFF Al)
(rng ll) \/ {()} is finite Element of bool (CQC-WFF Al)

rng ll is finite Element of bool (CQC-WFF Al)

ll " {()} is finite Element of bool NAT
dom ll is finite Element of bool NAT
JH is finite set

Seg (card JH) is finite card JH -element Element of bool NAT
K253((Seg (card JH)),()) is Relation-like Seg (card JH) -defined {()} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card JH)),{()}:]
{()} is non empty trivial finite 1 -element set
[:(Seg (card JH)),{()}:] is finite set
bool [:(Seg (card JH)),{()}:] is non empty finite V43() set
(ll - {()}) ^ (IdFinS ((),(card JH))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rel is finite set

Seg (len ll) is finite len ll -element Element of bool NAT

a - (len (ll - {()})) is ext-real V32() V37() integer set
seq ((len (ll - {()})),(card JH)) is Element of bool NAT

i is ext-real V32() V37() integer set

dom (Sgm JH) is finite Element of bool NAT
a is set

ll . i is set
rel \ JH is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (ll - {()})) is finite len (ll - {()}) -element Element of bool NAT

C is finite set

(card rel) - (card JH) is ext-real V32() V37() integer set

(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set
(len ll) - (card JH) is ext-real V32() V37() integer set
len ((ll - {()}) ^ (IdFinS ((),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((ll - {()}) ^ (IdFinS ((),(card JH))))) is finite len ((ll - {()}) ^ (IdFinS ((),(card JH)))) -element Element of bool NAT

(Sgm (rel \ JH)) . F is set
F - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {()}))) is set
F is set
F is set

F is set

dom (Sgm C) is finite Element of bool NAT

rng F is finite set
F is set

F . F is set
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
rng (Sgm JH) is finite Element of bool NAT
F - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {()}))) is set
(Seg (len (ll - {()}))) \/ (seq ((len (ll - {()})),(card JH))) is Element of bool NAT
F is set
F is set

(Sgm C) . F is set

F . F is set

(Sgm JH) . F is set

(len (ll - {()})) + (len (IdFinS ((),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((ll - {()}) ^ (IdFinS ((),(card JH)))) is finite Element of bool NAT
(F + (len (ll - {()}))) - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . ((F + (len (ll - {()}))) - (len (ll - {()}))) is set
F . (F + (len (ll - {()}))) is set
(len (ll - {()})) + (len (IdFinS ((),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len ll) - (card JH)) + (len (IdFinS ((),(card JH)))) is ext-real V32() V37() integer set
((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel

F is set
dom F is finite set
F . F is set
j is set
F . j is set
dom F is finite Element of bool rel
(Seg (len (ll - {()}))) \/ (seq ((len (ll - {()})),(card JH))) is Element of bool NAT
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT

h - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {()}))) is set
rng (Sgm JH) is finite Element of bool NAT
(Sgm C) . j is set

h - (len (ll - {()})) is ext-real V32() V37() integer set

k - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . (k - (len (ll - {()}))) is set
(Sgm JH) . (h - (len (ll - {()}))) is set
[:(dom ll),(dom ll):] is finite set
bool [:(dom ll),(dom ll):] is non empty finite V43() set

dom F is finite Element of bool (dom ll)
bool (dom ll) is non empty finite V43() set

F . j is set

dom (Per (ll,F)) is finite Element of bool NAT
dom ((ll - {()}) ^ (IdFinS ((),(card JH)))) is finite Element of bool NAT

F * ll is Relation-like dom ll -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom ll),(CQC-WFF Al):]
[:(dom ll),(CQC-WFF Al):] is set
bool [:(dom ll),(CQC-WFF Al):] is non empty set
dom (F * ll) is finite Element of bool (dom ll)
dom (IdFinS ((),(card JH))) is finite card JH -element Element of bool NAT

F . h is set
h - (len (ll - {()})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {()}))) is set
rng (Sgm JH) is finite Element of bool NAT
ll . (F . h) is set
(F * ll) . h is set
(Per (ll,F)) . h is set
(IdFinS ((),(card JH))) . k is set
((ll - {()}) ^ (IdFinS ((),(card JH)))) . h is set
dom (ll - {()}) is finite Element of bool NAT
(Sgm C) . h is set
ll . ((Sgm C) . h) is set

[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
((Sgm C) * ll) . h is set
(ll - {()}) . h is set
(F * ll) . j is set

h . j is set
(ll - {()}) . j is set
rng (ll - {()}) is finite set
(rng ll) \ {()} is finite Element of bool (CQC-WFF Al)

rng g is finite Element of bool (CQC-WFF Al)
(k \/ {()}) \ {()} is Element of bool (CQC-WFF Al)
k \ {()} is Element of bool (CQC-WFF Al)

Al is non empty Relation-like QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {P} is Element of bool (CQC-WFF Al)

rng ll is finite Element of bool (CQC-WFF Al)

dom <*P*> is non empty trivial finite 1 -element Element of bool NAT

dom (Ant ((ll ^ <*P*>) ^ <*P*>)) is finite Element of bool NAT
Suc ((ll ^ <*P*>) ^ <*P*>) is Element of CQC-WFF Al
(Ant ((ll ^ <*P*>) ^ <*P*>)) . ((len ll) + 1) is set

Suc (ll ^ <*P*>) is Element of CQC-WFF Al
rng (ll ^ <*P*>) is finite Element of bool (CQC-WFF Al)
(rng ll) \/ {P} is finite Element of bool (CQC-WFF Al)

rng ll is finite Element of bool (CQC-WFF Al)

ll " {P} is finite Element of bool NAT
dom ll is finite Element of bool NAT
JH is finite set

Seg (card JH) is finite card JH -element Element of bool NAT

{P} is non empty trivial finite 1 -element set
[:(Seg (card JH)),{P}:] is finite set
bool [:(Seg (card JH)),{P}:] is non empty finite V43() set

rel is finite set

Seg (len ll) is finite len ll -element Element of bool NAT

a - (len (ll - {P})) is ext-real V32() V37() integer set
seq ((len (ll - {P})),(card JH)) is Element of bool NAT

i is ext-real V32() V37() integer set

dom (Sgm JH) is finite Element of bool NAT
a is set

ll . i is set
rel \ JH is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (ll - {P})) is finite len (ll - {P}) -element Element of bool NAT

C is finite set

(card rel) - (card JH) is ext-real V32() V37() integer set

(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set
(len ll) - (card JH) is ext-real V32() V37() integer set
len ((ll - {P}) ^ (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((ll - {P}) ^ (IdFinS (P,(card JH))))) is finite len ((ll - {P}) ^ (IdFinS (P,(card JH)))) -element Element of bool NAT

(Sgm (rel \ JH)) . F is set
F - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {P}))) is set
F is set
F is set

F is set

dom (Sgm C) is finite Element of bool NAT

rng F is finite set
F is set

F . F is set
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
rng (Sgm JH) is finite Element of bool NAT
F - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {P}))) is set
(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT
F is set
F is set

(Sgm C) . F is set

F . F is set

(Sgm JH) . F is set

(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((ll - {P}) ^ (IdFinS (P,(card JH)))) is finite Element of bool NAT
(F + (len (ll - {P}))) - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . ((F + (len (ll - {P}))) - (len (ll - {P}))) is set
F . (F + (len (ll - {P}))) is set
(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len ll) - (card JH)) + (len (IdFinS (P,(card JH)))) is ext-real V32() V37() integer set
((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel

F is set
dom F is finite set
F . F is set
j is set
F . j is set
dom F is finite Element of bool rel
(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT

h - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {P}))) is set
rng (Sgm JH) is finite Element of bool NAT
(Sgm C) . j is set

h - (len (ll - {P})) is ext-real V32() V37() integer set

k - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (k - (len (ll - {P}))) is set
(Sgm JH) . (h - (len (ll - {P}))) is set
(k - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set
(h - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set
[:(dom ll),(dom ll):] is finite set
bool [:(dom ll),(dom ll):] is non empty finite V43() set

dom F is finite Element of bool (dom ll)
bool (dom ll) is non empty finite V43() set

F .