REAL is V35() V36() V37() V41() set
NAT is non trivial ordinal V35() V36() V37() V38() V39() V40() V41() V56() cardinal limit_cardinal Element of K32(REAL)
K32(REAL) is set
COMPLEX is V35() V41() set
NAT is non trivial ordinal V35() V36() V37() V38() V39() V40() V41() V56() cardinal limit_cardinal set
K32(NAT) is non trivial V56() set
{} is empty ordinal natural V24() ext-real non negative V32() V35() V36() V37() V38() V39() V40() V41() V56() V60() cardinal {} -element set
1 is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
{{},1} is non empty V35() V36() V37() V38() V39() V40() V56() V60() set
K32(NAT) is non trivial V56() set
{{}} is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
0 is empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V41() V56() V60() cardinal {} -element Element of NAT
dom {} is set
rng {} is set
the empty trivial finite {} -element RelStr is empty trivial finite {} -element RelStr
A is RelStr
the carrier of A is set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of K32(K33( the carrier of A, the carrier of A))
K33( the carrier of A, the carrier of A) is set
K32(K33( the carrier of A, the carrier of A)) is set
f is set
c3 is set
b is set
[f,c3] is set
{f,c3} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,c3},{f}} is non empty V56() V60() set
[c3,b] is set
{c3,b} is non empty V56() set
{c3} is non empty trivial V56() 1 -element set
{{c3,b},{c3}} is non empty V56() V60() set
[f,b] is set
{f,b} is non empty V56() set
{{f,b},{f}} is non empty V56() V60() set
f is set
c3 is set
[f,c3] is set
{f,c3} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,c3},{f}} is non empty V56() V60() set
[c3,f] is set
{c3,f} is non empty V56() set
{c3} is non empty trivial V56() 1 -element set
{{c3,f},{c3}} is non empty V56() V60() set
f is set
[f,f] is set
{f,f} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,f},{f}} is non empty V56() V60() set
A is ()
the non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr is non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr
A is non empty V80() reflexive transitive antisymmetric ()
the non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr is non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr
the finite V80() reflexive transitive antisymmetric () is finite V80() reflexive transitive antisymmetric ()
the carrier of the finite V80() reflexive transitive antisymmetric () is V56() set
A is non empty connected RelStr
f is non empty SubRelStr of A
the carrier of f is non empty set
c3 is Element of the carrier of f
b is Element of the carrier of f
the carrier of A is non empty set
B is Element of the carrier of A
Ab is Element of the carrier of A
A is finite RelStr
f is SubRelStr of A
the carrier of f is set
the carrier of A is V56() set
A is ordinal natural V24() ext-real non negative V32() V56() cardinal set
f is ordinal natural V24() ext-real non negative V32() V56() cardinal set
InclPoset A is strict V80() reflexive transitive antisymmetric RelStr
InclPoset f is strict V80() reflexive transitive antisymmetric RelStr
the InternalRel of (InclPoset f) is Relation-like the carrier of (InclPoset f) -defined the carrier of (InclPoset f) -valued V28( the carrier of (InclPoset f)) reflexive antisymmetric transitive Element of K32(K33( the carrier of (InclPoset f), the carrier of (InclPoset f)))
the carrier of (InclPoset f) is set
K33( the carrier of (InclPoset f), the carrier of (InclPoset f)) is set
K32(K33( the carrier of (InclPoset f), the carrier of (InclPoset f))) is set
RelIncl f is Relation-like f -defined f -valued V28(f) reflexive antisymmetric transitive V56() Element of K32(K33(f,f))
K33(f,f) is V56() set
K32(K33(f,f)) is V56() V60() set
RelIncl A is Relation-like A -defined A -valued V28(A) reflexive antisymmetric transitive V56() Element of K32(K33(A,A))
K33(A,A) is V56() set
K32(K33(A,A)) is V56() V60() set
c3 is set
(RelIncl f) |_2 A is Relation-like set
(RelIncl f) /\ K33(A,A) is V56() set
the carrier of (InclPoset A) is set
the InternalRel of (InclPoset A) is Relation-like the carrier of (InclPoset A) -defined the carrier of (InclPoset A) -valued V28( the carrier of (InclPoset A)) reflexive antisymmetric transitive Element of K32(K33( the carrier of (InclPoset A), the carrier of (InclPoset A)))
K33( the carrier of (InclPoset A), the carrier of (InclPoset A)) is set
K32(K33( the carrier of (InclPoset A), the carrier of (InclPoset A))) is set
(RelIncl f) |_2 A is Relation-like set
(RelIncl f) /\ K33(A,A) is V56() set
the InternalRel of (InclPoset f) |_2 the carrier of (InclPoset A) is Relation-like set
the InternalRel of (InclPoset f) /\ K33( the carrier of (InclPoset A), the carrier of (InclPoset A)) is set
A is RelStr
f is set
c3 is set
f /\ c3 is set
b is set
f \/ c3 is set
the carrier of A is set
Ab is Element of the carrier of A
A is non empty antisymmetric upper-bounded RelStr
the carrier of A is non empty set
Top A is Element of the carrier of A
{(Top A)} is non empty trivial V56() 1 -element Element of K32( the carrier of A)
K32( the carrier of A) is set
the carrier of A \ {(Top A)} is Element of K32( the carrier of A)
f is Element of the carrier of A
c3 is Element of the carrier of A
( the carrier of A \ {(Top A)}) \/ {(Top A)} is non empty Element of K32( the carrier of A)
A is RelStr
the carrier of A is set
f is RelStr
the carrier of f is set
K33( the carrier of A, the carrier of f) is set
K32(K33( the carrier of A, the carrier of f)) is set
c3 is Relation-like the carrier of A -defined the carrier of f -valued Function-like V29( the carrier of A, the carrier of f) Element of K32(K33( the carrier of A, the carrier of f))
A is antisymmetric RelStr
the carrier of A is set
K32( the carrier of A) is set
f is antisymmetric RelStr
the carrier of f is set
K32( the carrier of f) is set
K33( the carrier of A, the carrier of f) is set
K32(K33( the carrier of A, the carrier of f)) is set
c3 is Element of K32( the carrier of A)
b is Element of K32( the carrier of A)
subrelstr c3 is strict antisymmetric full SubRelStr of A
the carrier of (subrelstr c3) is set
subrelstr b is strict antisymmetric full SubRelStr of A
the carrier of (subrelstr b) is set
c3 \/ b is Element of K32( the carrier of A)
Ab is Element of K32( the carrier of f)
B is Element of K32( the carrier of f)
subrelstr Ab is strict antisymmetric full SubRelStr of f
the carrier of (subrelstr Ab) is set
K33( the carrier of (subrelstr c3), the carrier of (subrelstr Ab)) is set
K32(K33( the carrier of (subrelstr c3), the carrier of (subrelstr Ab))) is set
subrelstr B is strict antisymmetric full SubRelStr of f
the carrier of (subrelstr B) is set
K33( the carrier of (subrelstr b), the carrier of (subrelstr B)) is set
K32(K33( the carrier of (subrelstr b), the carrier of (subrelstr B))) is set
Ab \/ B is Element of K32( the carrier of f)
f is Relation-like the carrier of (subrelstr c3) -defined the carrier of (subrelstr Ab) -valued Function-like V29( the carrier of (subrelstr c3), the carrier of (subrelstr Ab)) Element of K32(K33( the carrier of (subrelstr c3), the carrier of (subrelstr Ab)))
n9 is Relation-like the carrier of (subrelstr b) -defined the carrier of (subrelstr B) -valued Function-like V29( the carrier of (subrelstr b), the carrier of (subrelstr B)) Element of K32(K33( the carrier of (subrelstr b), the carrier of (subrelstr B)))
f +* n9 is Relation-like Function-like set
dom f is set
b9 is set
(f +* n9) . b9 is set
dom n9 is set
dom (f +* n9) is set
b9 is Relation-like the carrier of A -defined the carrier of f -valued Function-like V29( the carrier of A, the carrier of f) Element of K32(K33( the carrier of A, the carrier of f))
dom n9 is set
dom f is set
dom (f +* n9) is set
(dom f) \/ (dom n9) is set
rng (f +* n9) is set
rng f is set
rng n9 is set
(rng f) \/ (rng n9) is set
b9 is set
X9 is set
f . X9 is set
(f +* n9) . X9 is set
X9 is set
n9 . X9 is set
(f +* n9) . X9 is set
b9 is set
(f +* n9) . b9 is set
X9 is non empty RelStr
the carrier of X9 is non empty set
b9 is non empty RelStr
the carrier of b9 is non empty set
K33( the carrier of X9, the carrier of b9) is set
K32(K33( the carrier of X9, the carrier of b9)) is set
g is Relation-like the carrier of X9 -defined the carrier of b9 -valued Function-like V29( the carrier of X9, the carrier of b9) Element of K32(K33( the carrier of X9, the carrier of b9))
g is Element of the carrier of X9
A2 is Element of the carrier of X9
g . g is Element of the carrier of b9
g . A2 is Element of the carrier of b9
K32( the carrier of b9) is set
K32( the carrier of X9) is set
e is non empty Element of K32( the carrier of X9)
subrelstr e is non empty strict full SubRelStr of X9
the carrier of (subrelstr e) is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of (subrelstr g) is non empty set
K33( the carrier of (subrelstr e), the carrier of (subrelstr g)) is set
K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g))) is set
f . g is set
f . A2 is set
f is Element of the carrier of (subrelstr e)
f1 is Element of the carrier of (subrelstr e)
e1 is Relation-like the carrier of (subrelstr e) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr e), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g)))
e1 . f is Element of the carrier of (subrelstr g)
e1 . f1 is Element of the carrier of (subrelstr g)
K32( the carrier of b9) is set
K32( the carrier of X9) is set
f is non empty Element of K32( the carrier of X9)
subrelstr f is non empty strict full SubRelStr of X9
the carrier of (subrelstr f) is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of (subrelstr g) is non empty set
K33( the carrier of (subrelstr f), the carrier of (subrelstr g)) is set
K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr g))) is set
f1 is non empty Element of K32( the carrier of X9)
subrelstr f1 is non empty strict full SubRelStr of X9
the carrier of (subrelstr f1) is non empty set
e is non empty Element of K32( the carrier of b9)
subrelstr e is non empty strict full SubRelStr of b9
the carrier of (subrelstr e) is non empty set
K33( the carrier of (subrelstr f1), the carrier of (subrelstr e)) is set
K32(K33( the carrier of (subrelstr f1), the carrier of (subrelstr e))) is set
e1 is Relation-like the carrier of (subrelstr f) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr f), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr g)))
ax is Element of the carrier of (subrelstr f)
e1 . ax is Element of the carrier of (subrelstr g)
g9 is Relation-like the carrier of (subrelstr f1) -defined the carrier of (subrelstr e) -valued Function-like V29( the carrier of (subrelstr f1), the carrier of (subrelstr e)) Element of K32(K33( the carrier of (subrelstr f1), the carrier of (subrelstr e)))
ay is Element of the carrier of (subrelstr f1)
g9 . ay is Element of the carrier of (subrelstr e)
f . g is set
n9 . A2 is set
n9 . g is set
f . A2 is set
K32( the carrier of b9) is set
K32( the carrier of X9) is set
e is non empty Element of K32( the carrier of X9)
subrelstr e is non empty strict full SubRelStr of X9
the carrier of (subrelstr e) is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of (subrelstr g) is non empty set
K33( the carrier of (subrelstr e), the carrier of (subrelstr g)) is set
K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g))) is set
n9 . g is set
n9 . A2 is set
f is Element of the carrier of (subrelstr e)
f1 is Element of the carrier of (subrelstr e)
e1 is Relation-like the carrier of (subrelstr e) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr e), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g)))
e1 . f is Element of the carrier of (subrelstr g)
e1 . f1 is Element of the carrier of (subrelstr g)
g is Element of the carrier of X9
g . g is Element of the carrier of b9
A2 is Element of the carrier of X9
g . A2 is Element of the carrier of b9
f . g is set
f . A2 is set
f . g is set
n9 . A2 is set
f . A2 is set
n9 . g is set
n9 . g is set
n9 . A2 is set
A is ordinal natural V24() ext-real non negative V32() V56() cardinal set
InclPoset A is strict V80() reflexive transitive antisymmetric RelStr
A + 1 is non empty ordinal natural V24() ext-real non negative V32() V56() cardinal set
InclPoset (A + 1) is non empty strict V80() reflexive transitive antisymmetric RelStr
0 + 1 is non empty ordinal natural V24() ext-real non negative V32() V56() cardinal set
f is finite V80() reflexive transitive antisymmetric ()
the carrier of f is V56() set
card the carrier of f is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
c3 is non empty finite V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() ()
Top c3 is Element of the carrier of c3
the carrier of c3 is non empty V56() set
Ab is set
{Ab} is non empty trivial V56() 1 -element set
InclPoset 1 is non empty strict V80() reflexive transitive antisymmetric RelStr
the carrier of c3 --> 0 is Relation-like the carrier of c3 -defined {0} -valued Function-like V29( the carrier of c3,{0}) V56() Element of K32(K33( the carrier of c3,{0}))
{0} is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
K33( the carrier of c3,{0}) is V56() set
K32(K33( the carrier of c3,{0})) is V56() V60() set
rng ( the carrier of c3 --> 0) is V56() set
the carrier of (InclPoset 1) is non empty set
K33( the carrier of c3, the carrier of (InclPoset 1)) is set
K32(K33( the carrier of c3, the carrier of (InclPoset 1))) is set
f is Relation-like the carrier of c3 -defined the carrier of (InclPoset 1) -valued Function-like V29( the carrier of c3, the carrier of (InclPoset 1)) V56() Element of K32(K33( the carrier of c3, the carrier of (InclPoset 1)))
n9 is Element of the carrier of c3
X is Element of the carrier of c3
f . n9 is Element of the carrier of (InclPoset 1)
f . X is Element of the carrier of (InclPoset 1)
n9 is Element of the carrier of c3
f . n9 is Element of the carrier of (InclPoset 1)
X is Element of the carrier of c3
f . X is Element of the carrier of (InclPoset 1)
{(Top c3)} is non empty trivial V56() 1 -element Element of K32( the carrier of c3)
K32( the carrier of c3) is V56() V60() set
the carrier of c3 \ {(Top c3)} is V56() Element of K32( the carrier of c3)
card ( the carrier of c3 \ {(Top c3)}) is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
card the carrier of c3 is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
card {(Top c3)} is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
(card the carrier of c3) - (card {(Top c3)}) is V24() ext-real V32() set
(A + 1) - 1 is V24() ext-real V32() set
1 - 1 is V24() ext-real V32() set
Ab is non empty V56() Element of K32( the carrier of c3)
subrelstr Ab is non empty finite strict V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() full connected V204() V205() SubRelStr of c3
B is finite V80() reflexive transitive antisymmetric ()
the carrier of B is V56() set
card the carrier of B is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of (InclPoset A) is set
K33( the carrier of B, the carrier of (InclPoset A)) is set
K32(K33( the carrier of B, the carrier of (InclPoset A))) is set
f is Relation-like the carrier of B -defined the carrier of (InclPoset A) -valued Function-like V29( the carrier of B, the carrier of (InclPoset A)) V56() Element of K32(K33( the carrier of B, the carrier of (InclPoset A)))
succ A is set
{A} is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
A \/ {A} is non empty V56() set
the carrier of (InclPoset (A + 1)) is non empty set
K32( the carrier of (InclPoset (A + 1))) is set
InclPoset {(Top c3)} is non empty strict V80() reflexive transitive antisymmetric RelStr
n9 is non empty Element of K32( the carrier of (InclPoset (A + 1)))
subrelstr n9 is non empty strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset (A + 1)
the carrier of (subrelstr n9) is non empty set
the carrier of (InclPoset {(Top c3)}) is non empty set
K32( the carrier of (InclPoset {(Top c3)})) is set
b9 is non empty Element of K32( the carrier of (InclPoset {(Top c3)}))
subrelstr b9 is non empty strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset {(Top c3)}
the carrier of (subrelstr b9) is non empty set
the carrier of (subrelstr b9) --> A is Relation-like the carrier of (subrelstr b9) -defined {A} -valued Function-like V29( the carrier of (subrelstr b9),{A}) Element of K32(K33( the carrier of (subrelstr b9),{A}))
K33( the carrier of (subrelstr b9),{A}) is set
K32(K33( the carrier of (subrelstr b9),{A})) is set
dom ( the carrier of (subrelstr b9) --> A) is set
A2 is Element of the carrier of (InclPoset (A + 1))
g is Element of the carrier of (InclPoset (A + 1))
{ b1 where b1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT : not A <= b1 } is set
e is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
f is set
{ b1 where b1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT : not e <= b1 } is set
f1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of (InclPoset A) \/ {A} is non empty set
subrelstr {(Top c3)} is non empty finite strict V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() full connected V204() V205() SubRelStr of c3
the carrier of (subrelstr {(Top c3)}) is non empty V56() set
K33( the carrier of (subrelstr {(Top c3)}), the carrier of (subrelstr n9)) is set
K32(K33( the carrier of (subrelstr {(Top c3)}), the carrier of (subrelstr n9))) is set
g is Relation-like the carrier of (subrelstr b9) -defined Function-like V28( the carrier of (subrelstr b9)) set
g is Relation-like the carrier of (subrelstr {(Top c3)}) -defined the carrier of (subrelstr n9) -valued Function-like V29( the carrier of (subrelstr {(Top c3)}), the carrier of (subrelstr n9)) V56() Element of K32(K33( the carrier of (subrelstr {(Top c3)}), the carrier of (subrelstr n9)))
g . (Top c3) is set
rng g is V56() set
e is Element of the carrier of (subrelstr {(Top c3)})
f is Element of the carrier of (subrelstr {(Top c3)})
g . e is Element of the carrier of (subrelstr n9)
g . f is Element of the carrier of (subrelstr n9)
e1 is Element of the carrier of (subrelstr b9)
g . e1 is set
f1 is Element of the carrier of (subrelstr b9)
g . f1 is set
A2 is Element of K32( the carrier of (InclPoset (A + 1)))
subrelstr A2 is strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset (A + 1)
K33( the carrier of c3, the carrier of (InclPoset (A + 1))) is set
K32(K33( the carrier of c3, the carrier of (InclPoset (A + 1)))) is set
f +* g is Relation-like Function-like V56() set
e is Relation-like the carrier of c3 -defined the carrier of (InclPoset (A + 1)) -valued Function-like V29( the carrier of c3, the carrier of (InclPoset (A + 1))) V56() Element of K32(K33( the carrier of c3, the carrier of (InclPoset (A + 1))))
InclPoset 0 is strict V80() reflexive transitive antisymmetric RelStr
A is finite V80() reflexive transitive antisymmetric ()
the carrier of A is V56() set
card the carrier of A is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of (InclPoset 0) is set
K33( the carrier of A, the carrier of (InclPoset 0)) is set
K32(K33( the carrier of A, the carrier of (InclPoset 0))) is set
the Relation-like the carrier of A -defined the carrier of (InclPoset 0) -valued Function-like V29( the carrier of A, the carrier of (InclPoset 0)) V56() Element of K32(K33( the carrier of A, the carrier of (InclPoset 0))) is Relation-like the carrier of A -defined the carrier of (InclPoset 0) -valued Function-like V29( the carrier of A, the carrier of (InclPoset 0)) V56() Element of K32(K33( the carrier of A, the carrier of (InclPoset 0)))
A is finite V80() reflexive transitive antisymmetric ()
the carrier of A is V56() set
card the carrier of A is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
f is ordinal natural V24() ext-real non negative V32() V56() cardinal set
InclPoset f is strict V80() reflexive transitive antisymmetric RelStr