REAL is V129() V130() V131() V135() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() Element of K26(REAL)
K26(REAL) is non empty set
COMPLEX is V129() V135() set
omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() set
K26(omega) is non empty V14() non finite set
K26(NAT) is non empty V14() non finite set
RAT is V129() V130() V131() V132() V135() set
INT is V129() V130() V131() V132() V133() V135() set
K27(REAL,REAL) is Relation-like set
K26(K27(REAL,REAL)) is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set
len omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal set
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() V18() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V118() V129() V130() V131() V132() V133() V134() V135() V140() V143() Element of NAT
Seg 1 is non empty V14() finite 1 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{1} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
Seg 2 is non empty finite 2 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{1,2} is non empty finite V36() V129() V130() V131() V132() V133() V134() V143() set
m is set
K26(m) is non empty set
r is set
the_subsets_of_card (r,m) is Element of K26(K26(m))
K26(K26(m)) is non empty set
{ b1 where b1 is Element of K26(m) : len b1 = r } is set
r is V14() non finite set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(r) is non empty V14() non finite set
K26(K26(r)) is non empty V14() non finite set
{ b1 where b1 is Element of K26(r) : len b1 = m } is set
len r is epsilon-transitive epsilon-connected ordinal V14() non finite cardinal set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
r is set
X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty set
P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
len r is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b1 where b1 is Element of K26(r) : len b1 = m } is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set
K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set
P9 is non empty set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
F1 is set
F is set
F1 . F is set
F is Element of P9
P .: F is set
Funcs (r,X) is functional set
rng P is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
S is Element of K26(X)
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of K26(r)
len h is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
F is Element of the_subsets_of_card (m,r)
F1 . F is set
P .: F is set
X9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
P9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
F1 is set
X9 . F1 is set
F1 is Element of the_subsets_of_card (m,r)
P .: F1 is set
P9 . F1 is set
m is set
r is set
X is set
the_subsets_of_card (X,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b1 where b1 is Element of K26(m) : len b1 = X } is set
the_subsets_of_card (X,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b1 where b1 is Element of K26(r) : len b1 = X } is set
P is set
X9 is Element of K26(m)
len X9 is epsilon-transitive epsilon-connected ordinal cardinal set
P9 is Element of K26(r)
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
r is set
K26(r) is non empty set
len r is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty set
P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))
(m,r,X,P) is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(K26(r)) is non empty set
{ b1 where b1 is Element of K26(r) : len b1 = m } is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set
K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set
X9 is Element of K26(r)
P .: X9 is set
the_subsets_of_card (m,(P .: X9)) is Element of K26(K26((P .: X9)))
K26((P .: X9)) is non empty set
K26(K26((P .: X9))) is non empty set
{ b1 where b1 is Element of K26((P .: X9)) : len b1 = m } is set
the_subsets_of_card (m,X9) is Element of K26(K26(X9))
K26(X9) is non empty set
K26(K26(X9)) is non empty set
{ b1 where b1 is Element of K26(X9) : len b1 = m } is set
(m,r,X,P) .: (the_subsets_of_card (m,X9)) is set
P9 is Relation-like Function-like set
P9 .: r is set
Funcs (r,X) is functional set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
F1 is Relation-like Function-like set
F1 .: X is set
P9 .: (F1 .: X) is set
F1 * P9 is Relation-like Function-like set
(F1 * P9) .: X is set
Funcs ((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is functional set
F1 is set
rng P is set
dom (m,r,X,P) is Element of K26((the_subsets_of_card (m,r)))
K26((the_subsets_of_card (m,r))) is non empty set
P " F1 is set
(m,r,X,P) . (P " F1) is set
dom P is Element of K26(r)
P .: (P " F1) is set
F is Element of K26(X9)
len F is epsilon-transitive epsilon-connected ordinal cardinal set
S is Element of K26((P .: X9))
len S is epsilon-transitive epsilon-connected ordinal cardinal set
S is Relation-like Function-like set
dom S is set
rng S is set
F is set
(m,r,X,P) . F is set
F is set
(m,r,X,P) . F is set
F is Element of the_subsets_of_card (m,r)
P .: F is set
h is Relation-like Function-like set
dom h is set
rng h is set
S is Element of K26((P .: X9))
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of K26(X9)
len h is epsilon-transitive epsilon-connected ordinal cardinal set
{0} is non empty V14() functional finite V36() 1 -element V129() V130() V131() V132() V133() V134() V141() V143() set
m is set
the_subsets_of_card (0,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b1 where b1 is Element of K26(m) : len b1 = 0 } is set
r is set
X is Element of K26(m)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
X is Element of K26(m)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
r is finite V143() set
card r is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
m is finite V143() set
the_subsets_of_card (m,r) is finite V36() V143() Element of K26(K26(r))
K26(r) is non empty finite V36() V143() set
K26(K26(r)) is non empty finite V36() V143() set
{ b1 where b1 is Element of K26(r) : len b1 = m } is set
{r} is non empty V14() finite V36() 1 -element V143() set
X is set
P is finite V143() Element of K26(r)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X9 is finite V143() Element of K26(r)
r \ X9 is finite V143() Element of K26(r)
card (r \ X9) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card r) - (card X9) is V16() V17() ext-real set
P is finite V143() Element of K26(r)
m is set
len m is epsilon-transitive epsilon-connected ordinal cardinal set
m is set
r is set
m \/ r is set
len m is epsilon-transitive epsilon-connected ordinal cardinal set
len (m \/ r) is epsilon-transitive epsilon-connected ordinal cardinal set
m is set
r is set
m \ r is Element of K26(m)
K26(m) is non empty set
m \/ r is set
(m \ r) \/ r is set
m is V14() non finite set
r is set
m \/ r is set
m is V14() non finite set
r is finite V143() set
m \ r is Element of K26(m)
K26(m) is non empty V14() non finite set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
K27((the_subsets_of_card (m,X)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,X)),r)) is non empty set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is set
the_subsets_of_card ((P + 1),P9) is Element of K26(K26(P9))
K26(P9) is non empty set
K26(K26(P9)) is non empty set
{ b1 where b1 is Element of K26(P9) : len b1 = P + 1 } is set
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
K27((the_subsets_of_card ((P + 1),P9)),X9) is Relation-like set
K26(K27((the_subsets_of_card ((P + 1),P9)),X9)) is non empty set
len P9 is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card (omega,P9) is Element of K26(K26(P9))
{ b1 where b1 is Element of K26(P9) : len b1 = omega } is set
F1 is non empty set
F1 is Relation-like the_subsets_of_card ((P + 1),P9) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card ((P + 1),P9)),X9))
min* P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S is set
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of S
{h} is non empty V14() finite 1 -element V143() set
S \ {h} is Element of K26(S)
K26(S) is non empty set
the_subsets_of_card (P,(S \ {h})) is Element of K26(K26((S \ {h})))
K26((S \ {h})) is non empty set
K26(K26((S \ {h}))) is non empty set
{ b1 where b1 is Element of K26((S \ {h})) : len b1 = P } is set
K27((the_subsets_of_card (P,(S \ {h}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(S \ {h}))),X9)) is non empty set
E is non empty set
E is Element of E
E \/ {h} is non empty set
F1 . (E \/ {h}) is set
x is Element of K26((S \ {h}))
len x is epsilon-transitive epsilon-connected ordinal cardinal set
(S \ {h}) \/ {h} is non empty set
S \/ {h} is non empty set
x99 is finite V143() set
x9 is Element of K26(S)
len x9 is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card ((P + 1),S) is Element of K26(K26(S))
K26(K26(S)) is non empty set
{ b1 where b1 is Element of K26(S) : len b1 = P + 1 } is set
K27(E,X9) is Relation-like set
K26(K27(E,X9)) is non empty set
E is Relation-like E -defined X9 -valued Function-like quasi_total Element of K26(K27(E,X9))
len (S \ {h}) is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))
x9 is Element of K26((S \ {h}))
the_subsets_of_card (P,x9) is Element of K26(K26(x9))
K26(x9) is non empty set
K26(K26(x9)) is non empty set
{ b1 where b1 is Element of K26(x9) : len b1 = P } is set
x | (the_subsets_of_card (P,x9)) is Relation-like the_subsets_of_card (P,(S \ {h})) -defined the_subsets_of_card (P,x9) -defined the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))
x99 is Element of the_subsets_of_card (P,(S \ {h}))
x . x99 is set
x99 \/ {h} is non empty set
F1 . (x99 \/ {h}) is set
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h is Element of F1
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of h
{E} is non empty V14() finite 1 -element V143() set
h \ {E} is Element of K26(h)
K26(h) is non empty set
the_subsets_of_card (P,(h \ {E})) is Element of K26(K26((h \ {E})))
K26((h \ {E})) is non empty set
K26(K26((h \ {E}))) is non empty set
{ b1 where b1 is Element of K26((h \ {E})) : len b1 = P } is set
K27((the_subsets_of_card (P,(h \ {E}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(h \ {E}))),X9)) is non empty set
E is Element of K26(P9)
len E is epsilon-transitive epsilon-connected ordinal cardinal set
x is Element of K26((h \ {E}))
E is Relation-like the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))
the_subsets_of_card (P,x) is Element of K26(K26(x))
K26(x) is non empty set
K26(K26(x)) is non empty set
{ b1 where b1 is Element of K26(x) : len b1 = P } is set
E | (the_subsets_of_card (P,x)) is Relation-like the_subsets_of_card (P,(h \ {E})) -defined the_subsets_of_card (P,x) -defined the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))
len x is epsilon-transitive epsilon-connected ordinal cardinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( not b1 <= h & b1 in x ) } is set
min* { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( not b1 <= h & b1 in x ) } is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x9 is Element of F1
F9 is Element of F1
S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of F1
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
F9 \ {S9} is Element of K26(F9)
K26(F9) is non empty set
the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))
K26((F9 \ {S9})) is non empty set
K26(K26((F9 \ {S9}))) is non empty set
{ b1 where b1 is Element of K26((F9 \ {S9})) : len b1 = P } is set
K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set
x is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))
S99 is Element of K26((F9 \ {S9}))
the_subsets_of_card (P,S99) is Element of K26(K26(S99))
K26(S99) is non empty set
K26(K26(S99)) is non empty set
{ b1 where b1 is Element of K26(S99) : len b1 = P } is set
x | (the_subsets_of_card (P,S99)) is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined the_subsets_of_card (P,S99) -defined the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))
S999 is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S999 is V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b1 <= h & b1 in x ) } is set
s2 is set
S999 \/ { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b1 <= h & b1 in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s2 is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)
s2 is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b2 <= h & b2 in x ) } is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is Element of the_subsets_of_card (P,(F9 \ {S9}))
x . s1 is set
s1 \/ {S9} is non empty set
F1 . (s1 \/ {S9}) is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S99 is Element of F1
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
c24 is Element of F1
S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
S99 \ {x} is Element of K26(S99)
K26(S99) is non empty set
the_subsets_of_card (P,(S99 \ {x})) is Element of K26(K26((S99 \ {x})))
K26((S99 \ {x})) is non empty set
K26(K26((S99 \ {x}))) is non empty set
{ b1 where b1 is Element of K26((S99 \ {x})) : len b1 = P } is set
K27((the_subsets_of_card (P,(S99 \ {x}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(S99 \ {x}))),X9)) is non empty set
F9 is Element of F1
S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of F1
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
F9 \ {S9} is Element of K26(F9)
K26(F9) is non empty set
the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))
K26((F9 \ {S9})) is non empty set
K26(K26((F9 \ {S9}))) is non empty set
{ b1 where b1 is Element of K26((F9 \ {S9})) : len b1 = P } is set
K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set
E is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is Element of F1
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x99} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
x \ {x99} is Element of K26(x)
K26(x) is non empty set
the_subsets_of_card (P,(x \ {x99})) is Element of K26(K26((x \ {x99})))
K26((x \ {x99})) is non empty set
K26(K26((x \ {x99}))) is non empty set
{ b1 where b1 is Element of K26((x \ {x99})) : len b1 = P } is set
K27((the_subsets_of_card (P,(x \ {x99}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(x \ {x99}))),X9)) is non empty set
K27(NAT,F1) is Relation-like non empty V14() non finite set
K26(K27(NAT,F1)) is non empty V14() non finite set
K27(NAT,omega) is Relation-like non empty V14() non finite set
K26(K27(NAT,omega)) is non empty V14() non finite set
F is Element of F1
S is Relation-like NAT -defined F1 -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,F1))
S . 0 is Element of F1
h is Relation-like NAT -defined omega -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,omega))
h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . (0 + 1) is Element of F1
S . 0 is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of F1
{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
E \ {x9} is Element of K26(E)
K26(E) is non empty set
the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))
K26((E \ {x9})) is non empty set
K26(K26((E \ {x9}))) is non empty set
{ b1 where b1 is Element of K26((E \ {x9})) : len b1 = P } is set
K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S . (0 + 1) is Element of F1
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . (h + 1) is Element of F1
S . h is Element of F1
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(h + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . ((h + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . ((h + 1) + 1) is Element of F1
S . (h + 1) is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of F1
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
E \ {x9} is Element of K26(E)
K26(E) is non empty set
the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))
K26((E \ {x9})) is non empty set
K26(K26((E \ {x9}))) is non empty set
{ b1 where b1 is Element of K26((E \ {x9})) : len b1 = P } is set
K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set
S . E is Element of F1
S . E is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h + (E + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
0 + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
S . h is Element of F1
S . E is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
S . h is Element of F1
S . E is Element of F1
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E + x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . h is Element of F1
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . h)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . h) \ {(h . h)} is Element of K26((S . h))
K26((S . h)) is non empty set
the_subsets_of_card (P,((S . h) \ {(h . h)})) is Element of K26(K26(((S . h) \ {(h . h)})))
K26(((S . h) \ {(h . h)})) is non empty set
K26(K26(((S . h) \ {(h . h)}))) is non empty set
{ b1 where b1 is Element of K26(((S . h) \ {(h . h)})) : len b1 = P } is set
K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9)) is non empty set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= h ) } is set
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (h + 1) is Element of F1
E is set
the_subsets_of_card (P,E) is Element of K26(K26(E))
K26(E) is non empty set
K26(K26(E)) is non empty set
{ b1 where b1 is Element of K26(E) : len b1 = P } is set
E is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
E | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is Element of F1
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x99 is Element of F1
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{F9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
x99 \ {F9} is Element of K26(x99)
K26(x99) is non empty set
the_subsets_of_card (P,(x99 \ {F9})) is Element of K26(K26((x99 \ {F9})))
K26((x99 \ {F9})) is non empty set
K26(K26((x99 \ {F9}))) is non empty set
{ b1 where b1 is Element of K26((x99 \ {F9})) : len b1 = P } is set
K27((the_subsets_of_card (P,(x99 \ {F9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9)) is non empty set
S9 is Element of K26((x99 \ {F9}))
S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
S9 is Element of K26((x99 \ {F9}))
S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
S99 is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
S99 is Element of the_subsets_of_card (P,((S . h) \ {(h . h)}))
S99 . S99 is set
E . S99 is set
S99 \/ {(h . h)} is non empty set
F1 . (S99 \/ {(h . h)}) is set
the_subsets_of_card (P,(S . (h + 1))) is Element of K26(K26((S . (h + 1))))
K26((S . (h + 1))) is non empty set
K26(K26((S . (h + 1)))) is non empty set
{ b1 where b1 is Element of K26((S . (h + 1))) : len b1 = P } is set
E | (the_subsets_of_card (P,(S . (h + 1)))) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,(S . (h + 1))) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
S99 is set
c24 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
c24 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . c24 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . c24 is Element of F1
dom (E | (the_subsets_of_card (P,E))) is Element of K26((the_subsets_of_card (P,E)))
K26((the_subsets_of_card (P,E))) is non empty set
S99 is set
c24 is set
(E | (the_subsets_of_card (P,E))) . S99 is set
(E | (the_subsets_of_card (P,E))) . c24 is set
dom E is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))
K26((the_subsets_of_card (P,((S . h) \ {(h . h)})))) is non empty set
dom (E | (the_subsets_of_card (P,(S . (h + 1))))) is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))
(E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . S99 is set
(E | (the_subsets_of_card (P,(S . (h + 1))))) . S99 is set
(E | (the_subsets_of_card (P,(S . (h + 1))))) . c24 is set
((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . c24 is set
dom h is non empty V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
h is set
E is set
h . h is set
h . E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= h ) } is set
len { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= h ) } is epsilon-transitive epsilon-connected ordinal cardinal set
E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)
NAT \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
h | (NAT \ (Segm (h + 1))) is Relation-like NAT -defined NAT \ (Segm (h + 1)) -defined NAT -defined omega -valued Function-like Element of K26(K27(NAT,omega))
dom (h | (NAT \ (Segm (h + 1)))) is V129() V130() V131() V132() V133() V134() Element of K26((NAT \ (Segm (h + 1))))
K26((NAT \ (Segm (h + 1)))) is non empty set
(dom h) /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
NAT /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
NAT /\ NAT is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
(NAT /\ NAT) \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
rng (h | (NAT \ (Segm (h + 1)))) is set
E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is set
(h | (NAT \ (Segm (h + 1)))) . x is set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h is set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } is set
x is Element of S . E
{x} is non empty V14() finite 1 -element V143() set
(S . E) \ {x} is Element of K26((S . E))
K26((S . E)) is non empty set
the_subsets_of_card (P,((S . E) \ {x})) is Element of K26(K26(((S . E) \ {x})))
K26(((S . E) \ {x})) is non empty set
K26(K26(((S . E) \ {x}))) is non empty set
{ b1 where b1 is Element of K26(((S . E) \ {x})) : len b1 = P } is set
K27((the_subsets_of_card (P,((S . E) \ {x}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9)) is non empty set
x99 is Element of K26(P9)
len x99 is epsilon-transitive epsilon-connected ordinal cardinal set
F9 is Element of K26(((S . E) \ {x}))
x99 is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
the_subsets_of_card (P,F9) is Element of K26(K26(F9))
K26(F9) is non empty set
K26(K26(F9)) is non empty set
{ b1 where b1 is Element of K26(F9) : len b1 = P } is set
x99 | (the_subsets_of_card (P,F9)) is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P,F9) -defined the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
S9 is set
{(h . E)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . E) \ {(h . E)} is Element of K26((S . E))
the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ) is Element of K26(K26( { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ))
K26( { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ) is non empty set
K26(K26( { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } )) is non empty set
{ b1 where b1 is Element of K26( { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ) : len b1 = P } is set
x99 | (the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } )) is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ) -defined the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
K27((the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } )),X9) is Relation-like set
K26(K27((the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } )),X9)) is non empty set
len { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } is epsilon-transitive epsilon-connected ordinal cardinal set
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng (x99 | (the_subsets_of_card (P, { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b2 being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b2 = b1 & not b2 <= E ) } ))) is set
S9 is epsilon-transitive epsilon-connected ordinal Element of X9
{S9} is non empty V14() finite 1 -element V143() set
S9 is set
S99 is set
the_subsets_of_card (P,S99) is Element of K26(K26(S99))
K26(S99) is non empty set
K26(K26(S99)) is non empty set
{ b1 where b1 is Element of K26(S99) : len b1 = P } is set
c24 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . c24 is Element of F1
h . c24 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . c24)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . c24) \ {(h . c24)} is Element of K26((S . c24))
K26((S . c24)) is non empty set
the_subsets_of_card (P,((S . c24) \ {(h . c24)})) is Element of K26(K26(((S . c24) \ {(h . c24)})))
K26(((S . c24) \ {(h . c24)})) is non empty set
K26(K26(((S . c24) \ {(h . c24)}))) is non empty set
{ b1 where b1 is Element of K26(((S . c24) \ {(h . c24)})) : len b1 = P } is set
K27((the_subsets_of_card (P,((S . c24) \ {(h . c24)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . c24) \ {(h . c24)}))),X9)) is non empty set
{ b1 where b1 is epsilon-transitive epsilon-connected