:: GLIB_000 semantic presentation

REAL is set
NAT is non empty non trivial V24() V25() V26() non finite cardinal limit_cardinal Element of K32(REAL)
K32(REAL) is non empty set
COMPLEX is set
RAT is set
INT is set
K33(COMPLEX,COMPLEX) is Relation-like set
K32(K33(COMPLEX,COMPLEX)) is non empty set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K33(REAL,REAL) is Relation-like set
K32(K33(REAL,REAL)) is non empty set
K33(K33(REAL,REAL),REAL) is Relation-like set
K32(K33(K33(REAL,REAL),REAL)) is non empty set
K33(RAT,RAT) is Relation-like set
K32(K33(RAT,RAT)) is non empty set
K33(K33(RAT,RAT),RAT) is Relation-like set
K32(K33(K33(RAT,RAT),RAT)) is non empty set
K33(INT,INT) is Relation-like set
K32(K33(INT,INT)) is non empty set
K33(K33(INT,INT),INT) is Relation-like set
K32(K33(K33(INT,INT),INT)) is non empty set
K33(NAT,NAT) is non empty non trivial Relation-like non finite set
K33(K33(NAT,NAT),NAT) is non empty non trivial Relation-like non finite set
K32(K33(K33(NAT,NAT),NAT)) is non empty non trivial non finite set
NAT is non empty non trivial V24() V25() V26() non finite cardinal limit_cardinal set
K32(NAT) is non empty non trivial non finite set
K32(NAT) is non empty non trivial non finite set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() set
1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
4 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
5 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of NAT
dom {} is empty proper Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(NAT)
() is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
() is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
() is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
() is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
{(),(),(),()} is non empty finite Element of K32(NAT)
() is non empty Element of K32(NAT)
G is Relation-like NAT -defined Function-like finite set
G . () is set
G . () is set
G . () is set
G . () is set
{1} is non empty trivial finite V40() 1 -element Element of K32(NAT)
K33({},{1}) is Relation-like finite set
K32(K33({},{1})) is non empty finite V40() set
G2 is empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional V17( {} ) V18( {} ,{1}) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33({},{1}))
<*{1},{},G2,G2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
len <*{1},{},G2,G2*> is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
dom <*{1},{},G2,G2*> is non empty finite 4 -element Element of K32(NAT)
Seg 4 is non empty finite 4 -element Element of K32(NAT)
e is Relation-like NAT -defined Function-like finite set
dom e is finite Element of K32(NAT)
(e) is set
e . () is set
(e) is set
e . () is set
(e) is set
e . () is set
(e) is set
e . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
(G) is set
G . () is set
G1 is set
G is non empty set
K33(G1,G) is Relation-like set
K32(K33(G1,G)) is non empty set
G2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) Element of K32(K33(G1,G))
v2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) Element of K32(K33(G1,G))
<*G,G1,G2,v2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
len <*G,G1,G2,v2*> is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
dom <*G,G1,G2,v2*> is non empty finite 4 -element Element of K32(NAT)
Seg 4 is non empty finite 4 -element Element of K32(NAT)
v2 is Relation-like NAT -defined Function-like finite set
dom v2 is finite Element of K32(NAT)
(v2) is set
v2 . () is set
(v2) is set
v2 . () is set
(v2) is set
v2 . () is set
(v2) is set
v2 . () is set
G is Relation-like NAT -defined Function-like finite set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G2 is set
G1 .--> G2 is Relation-like {G1} -defined Function-like one-to-one finite set
{G1} is non empty trivial finite V40() 1 -element set
{G1} --> G2 is non empty Relation-like {G1} -defined {G2} -valued Function-like constant V17({G1}) V18({G1},{G2}) finite Element of K32(K33({G1},{G2}))
{G2} is non empty trivial finite 1 -element set
K33({G1},{G2}) is non empty Relation-like finite set
K32(K33({G1},{G2})) is non empty finite V40() set
G +* (G1 .--> G2) is Relation-like Function-like finite set
dom (G1 .--> G2) is trivial finite V40() Element of K32({G1})
K32({G1}) is non empty finite V40() set
dom (G +* (G1 .--> G2)) is finite set
dom G is finite Element of K32(NAT)
(dom G) \/ (dom (G1 .--> G2)) is finite set
G is Relation-like NAT -defined Function-like finite set
dom G is finite Element of K32(NAT)
(G) is set
G . () is set
(G) is set
G . () is set
(G) is set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
(G) is set
G . () is set
G1 is set
G is Relation-like NAT -defined Function-like finite () set
G | () is Relation-like () -defined NAT -defined Function-like finite set
G1 is set
dom G is finite Element of K32(NAT)
((G | ())) is set
(G | ()) . () is set
(G) is non empty set
G . () is set
((G | ())) is set
(G | ()) . () is set
(G) is set
G . () is set
((G | ())) is set
(G | ()) . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
((G | ())) is set
(G | ()) . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
dom (G | ()) is finite Element of K32(())
K32(()) is non empty set
(dom G) /\ () is finite Element of K32(NAT)
G is Relation-like NAT -defined Function-like finite () set
G2 is set
v2 is set
G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
v2 is set
e is set
G1 is set
G2 is set
G is Relation-like NAT -defined Function-like finite () set
v2 is set
e is set
G1 is set
G2 is set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
card (G) is non empty V24() V25() V26() cardinal set
G1 is set
{G1} is non empty trivial finite 1 -element set
(G) is set
G . () is set
(G) is set
G . () is set
G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
(G) is set
G . () is set
(G) is set
G . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
card (G) is non empty V24() V25() V26() cardinal set
G1 is set
{G1} is non empty trivial finite 1 -element set
(G) is set
G . () is set
choose (G) is Element of (G)
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . (choose (G)) is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . (choose (G)) is set
v2 is set
(G) . v2 is set
(G) . v2 is set
{(choose (G))} is non empty trivial finite 1 -element set
{1} is non empty trivial finite V40() 1 -element Element of K32(NAT)
K33({},{1}) is Relation-like finite set
K32(K33({},{1})) is non empty finite V40() set
G2 is empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional V17( {} ) V18( {} ,{1}) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33({},{1}))
({1},{},G2,G2) is Relation-like NAT -defined Function-like finite () set
<*{1},{},G2,G2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
(({1},{},G2,G2)) is non empty set
({1},{},G2,G2) . () is set
card (({1},{},G2,G2)) is non empty V24() V25() V26() cardinal set
(({1},{},G2,G2)) is set
({1},{},G2,G2) . () is set
Y is set
EV is set
e is set
v2 is set
(({1},{},G2,G2)) is Relation-like (({1},{},G2,G2)) -defined (({1},{},G2,G2)) -valued Function-like V17((({1},{},G2,G2))) V18((({1},{},G2,G2)),(({1},{},G2,G2))) Element of K32(K33((({1},{},G2,G2)),(({1},{},G2,G2))))
K33((({1},{},G2,G2)),(({1},{},G2,G2))) is Relation-like set
K32(K33((({1},{},G2,G2)),(({1},{},G2,G2)))) is non empty set
({1},{},G2,G2) . () is set
(({1},{},G2,G2)) is Relation-like (({1},{},G2,G2)) -defined (({1},{},G2,G2)) -valued Function-like V17((({1},{},G2,G2))) V18((({1},{},G2,G2)),(({1},{},G2,G2))) Element of K32(K33((({1},{},G2,G2)),(({1},{},G2,G2))))
({1},{},G2,G2) . () is set
e is set
(({1},{},G2,G2)) . e is set
(({1},{},G2,G2)) . e is set
{1,2} is non empty finite V40() Element of K32(NAT)
K33({},{1,2}) is Relation-like finite set
K32(K33({},{1,2})) is non empty finite V40() set
G2 is empty Relation-like non-empty empty-yielding {} -defined {1,2} -valued Function-like one-to-one constant functional V17( {} ) V18( {} ,{1,2}) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33({},{1,2}))
({1,2},{},G2,G2) is Relation-like NAT -defined Function-like finite () set
<*{1,2},{},G2,G2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
(({1,2},{},G2,G2)) is set
({1,2},{},G2,G2) . () is set
(({1,2},{},G2,G2)) is non empty set
({1,2},{},G2,G2) . () is set
card (({1,2},{},G2,G2)) is non empty V24() V25() V26() cardinal set
(({1,2},{},G2,G2)) is Relation-like (({1,2},{},G2,G2)) -defined (({1,2},{},G2,G2)) -valued Function-like V17((({1,2},{},G2,G2))) V18((({1,2},{},G2,G2)),(({1,2},{},G2,G2))) Element of K32(K33((({1,2},{},G2,G2)),(({1,2},{},G2,G2))))
K33((({1,2},{},G2,G2)),(({1,2},{},G2,G2))) is Relation-like set
K32(K33((({1,2},{},G2,G2)),(({1,2},{},G2,G2)))) is non empty set
({1,2},{},G2,G2) . () is set
(({1,2},{},G2,G2)) is Relation-like (({1,2},{},G2,G2)) -defined (({1,2},{},G2,G2)) -valued Function-like V17((({1,2},{},G2,G2))) V18((({1,2},{},G2,G2)),(({1,2},{},G2,G2))) Element of K32(K33((({1,2},{},G2,G2)),(({1,2},{},G2,G2))))
({1,2},{},G2,G2) . () is set
e is set
(({1,2},{},G2,G2)) . e is set
(({1,2},{},G2,G2)) . e is set
Y is set
EV is set
e is set
v2 is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty set
G . () is set
card (G) is non empty V24() V25() V26() cardinal set
G1 is finite set
G is non empty finite set
K33(G1,G) is Relation-like finite set
K32(K33(G1,G)) is non empty finite V40() set
G2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) finite Element of K32(K33(G1,G))
v2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) finite Element of K32(K33(G1,G))
(G,G1,G2,v2) is Relation-like NAT -defined Function-like finite () set
<*G,G1,G2,v2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((G,G1,G2,v2)) is non empty set
(G,G1,G2,v2) . () is set
((G,G1,G2,v2)) is set
(G,G1,G2,v2) . () is set
G1 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() set
G is non empty set
K33(G1,G) is Relation-like set
K32(K33(G1,G)) is non empty set
G2 is empty Relation-like non-empty empty-yielding G1 -defined G -valued Function-like one-to-one constant functional V17(G1) V18(G1,G) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33(G1,G))
v2 is empty Relation-like non-empty empty-yielding G1 -defined G -valued Function-like one-to-one constant functional V17(G1) V18(G1,G) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33(G1,G))
(G,G1,G2,v2) is Relation-like NAT -defined Function-like finite () set
<*G,G1,G2,v2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((G,G1,G2,v2)) is set
(G,G1,G2,v2) . () is set
EV is set
S is set
v2 is set
Y is set
((G,G1,G2,v2)) is Relation-like ((G,G1,G2,v2)) -defined ((G,G1,G2,v2)) -valued Function-like V17(((G,G1,G2,v2))) V18(((G,G1,G2,v2)),((G,G1,G2,v2))) Element of K32(K33(((G,G1,G2,v2)),((G,G1,G2,v2))))
((G,G1,G2,v2)) is non empty set
(G,G1,G2,v2) . () is set
K33(((G,G1,G2,v2)),((G,G1,G2,v2))) is Relation-like set
K32(K33(((G,G1,G2,v2)),((G,G1,G2,v2)))) is non empty set
(G,G1,G2,v2) . () is set
((G,G1,G2,v2)) is Relation-like ((G,G1,G2,v2)) -defined ((G,G1,G2,v2)) -valued Function-like V17(((G,G1,G2,v2))) V18(((G,G1,G2,v2)),((G,G1,G2,v2))) Element of K32(K33(((G,G1,G2,v2)),((G,G1,G2,v2))))
(G,G1,G2,v2) . () is set
v2 is set
((G,G1,G2,v2)) . v2 is set
((G,G1,G2,v2)) . v2 is set
G1 is set
G is set
{G} is non empty trivial finite 1 -element set
K33(G1,{G}) is Relation-like set
K32(K33(G1,{G})) is non empty set
G2 is Relation-like G1 -defined {G} -valued Function-like V17(G1) V18(G1,{G}) Element of K32(K33(G1,{G}))
v2 is Relation-like G1 -defined {G} -valued Function-like V17(G1) V18(G1,{G}) Element of K32(K33(G1,{G}))
({G},G1,G2,v2) is Relation-like NAT -defined Function-like finite () set
<*{G},G1,G2,v2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
(({G},G1,G2,v2)) is non empty set
({G},G1,G2,v2) . () is set
card (({G},G1,G2,v2)) is non empty V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
card (G) is non empty V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is V24() V25() V26() cardinal set
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
card (G) is V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is V24() V25() V26() cardinal set
(G) is finite set
G . () is set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
K32((G)) is non empty set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
G1 is set
G2 is Element of K32((G))
v2 is set
(G) . v2 is set
e is set
(G) . e is set
G2 is Element of K32((G))
v2 is Element of K32((G))
e is set
(G) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G2 is Element of K32((G))
v2 is set
(G) . v2 is set
e is set
(G) . e is set
G2 is Element of K32((G))
v2 is Element of K32((G))
e is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
G1 is set
(G,G1) is Element of K32((G))
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
K32((G)) is non empty set
G1 is set
G2 is set
v2 is Element of K32((G))
e is set
v2 is Element of K32((G))
e is Element of K32((G))
v2 is set
v2 is Element of K32((G))
e is set
v2 is Element of K32((G))
e is Element of K32((G))
v2 is set
G is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Relation-like NAT -defined Function-like finite () () set
(G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is non empty finite set
G1 . () is set
card (G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Relation-like NAT -defined Function-like finite () () set
(G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is non empty finite set
G1 . () is set
card (G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G1 is Relation-like NAT -defined Function-like finite () () set
(G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is finite set
G1 . () is set
card (G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () () set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is finite set
G . () is set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Relation-like NAT -defined Function-like finite () () set
(G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is finite set
G1 . () is set
card (G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G1) is set
G1 . () is set
(G) is set
G . () is set
K32((G)) is non empty set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
the Element of (G) is Element of (G)
{ the Element of (G)} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
K33({},{ the Element of (G)}) is Relation-like finite set
K32(K33({},{ the Element of (G)})) is non empty finite V40() set
e is empty Relation-like non-empty empty-yielding {} -defined { the Element of (G)} -valued Function-like one-to-one constant functional V17( {} ) V18( {} ,{ the Element of (G)}) ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V48() Element of K32(K33({},{ the Element of (G)}))
({ the Element of (G)},{},e,e) is Relation-like NAT -defined Function-like finite () () () () () () () () set
<*{ the Element of (G)},{},e,e*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
(({ the Element of (G)},{},e,e)) is non empty finite set
({ the Element of (G)},{},e,e) . () is set
(({ the Element of (G)},{},e,e)) is finite set
({ the Element of (G)},{},e,e) . () is set
(({ the Element of (G)},{},e,e)) is Relation-like (({ the Element of (G)},{},e,e)) -defined (({ the Element of (G)},{},e,e)) -valued Function-like V17((({ the Element of (G)},{},e,e))) V18((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e))) finite Element of K32(K33((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e))))
K33((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e))) is Relation-like finite set
K32(K33((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e)))) is non empty finite V40() set
({ the Element of (G)},{},e,e) . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(({ the Element of (G)},{},e,e)) is Relation-like (({ the Element of (G)},{},e,e)) -defined (({ the Element of (G)},{},e,e)) -valued Function-like V17((({ the Element of (G)},{},e,e))) V18((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e))) finite Element of K32(K33((({ the Element of (G)},{},e,e)),(({ the Element of (G)},{},e,e))))
({ the Element of (G)},{},e,e) . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
Y is set
(({ the Element of (G)},{},e,e)) . Y is set
(G) . Y is set
(({ the Element of (G)},{},e,e)) . Y is set
(G) . Y is set
Y is Relation-like NAT -defined Function-like finite () (G)
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is set
v2 is set
e is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty finite Element of K32((G))
(G) is non empty finite set
G . () is set
K32((G)) is non empty finite V40() set
G1 . () is set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
G1 . () is set
G is Relation-like NAT -defined Function-like finite () () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
G2 is set
(G1) . G2 is set
(G1) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is set
{G2} is non empty trivial finite 1 -element set
(G,G1) is non empty finite Element of K32((G))
K32((G)) is non empty finite V40() set
G1 . () is set
card (G,G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () () () set
G1 is Relation-like NAT -defined Function-like finite () (G)
e is set
v2 is set
G2 is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 . () is set
G2 is Relation-like NAT -defined Function-like finite () set
(G2) is non empty set
G2 . () is set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is set
v2 . () is set
e is Relation-like NAT -defined Function-like finite () set
(e) is set
e . () is set
(e) is non empty set
e . () is set
(e) is Relation-like (e) -defined (e) -valued Function-like V17((e)) V18((e),(e)) Element of K32(K33((e),(e)))
K33((e),(e)) is Relation-like set
K32(K33((e),(e))) is non empty set
e . () is set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is set
v2 . () is set
(v2) is non empty set
v2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
G2 is Relation-like NAT -defined Function-like finite () set
(G2) is non empty set
G2 . () is set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is non empty set
v2 . () is set
(G2) is set
G2 . () is set
(v2) is set
v2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
v2 . () is set
G2 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
K32((G)) is non empty set
G2 is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
v2 is Element of K32((G))
(G) | v2 is Relation-like (G) -defined v2 -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) | v2 is Relation-like (G) -defined v2 -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
dom (G) is Element of K32((G))
dom ((G) | v2) is Element of K32(v2)
K32(v2) is non empty set
EV is set
(G) . EV is set
((G) | v2) . EV is set
Y is non empty Element of K32((G))
K33(v2,Y) is Relation-like set
K32(K33(v2,Y)) is non empty set
dom (G) is Element of K32((G))
dom ((G) | v2) is Element of K32(v2)
S is set
(G) . S is set
((G) | v2) . S is set
S is Relation-like v2 -defined Y -valued Function-like V17(v2) V18(v2,Y) Element of K32(K33(v2,Y))
EV is Relation-like v2 -defined Y -valued Function-like V17(v2) V18(v2,Y) Element of K32(K33(v2,Y))
(Y,v2,S,EV) is Relation-like NAT -defined Function-like finite () set
<*Y,v2,S,EV*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((Y,v2,S,EV)) is set
(Y,v2,S,EV) . () is set
((Y,v2,S,EV)) is non empty set
(Y,v2,S,EV) . () is set
((Y,v2,S,EV)) is Relation-like ((Y,v2,S,EV)) -defined ((Y,v2,S,EV)) -valued Function-like V17(((Y,v2,S,EV))) V18(((Y,v2,S,EV)),((Y,v2,S,EV))) Element of K32(K33(((Y,v2,S,EV)),((Y,v2,S,EV))))
K33(((Y,v2,S,EV)),((Y,v2,S,EV))) is Relation-like set
K32(K33(((Y,v2,S,EV)),((Y,v2,S,EV)))) is non empty set
(Y,v2,S,EV) . () is set
((Y,v2,S,EV)) is Relation-like ((Y,v2,S,EV)) -defined ((Y,v2,S,EV)) -valued Function-like V17(((Y,v2,S,EV))) V18(((Y,v2,S,EV)),((Y,v2,S,EV))) Element of K32(K33(((Y,v2,S,EV)),((Y,v2,S,EV))))
(Y,v2,S,EV) . () is set
IT is set
((Y,v2,S,EV)) . IT is set
(G) . IT is set
((Y,v2,S,EV)) . IT is set
(G) . IT is set
IT is Relation-like NAT -defined Function-like finite () (G)
IT is Relation-like NAT -defined Function-like finite () (G)
(G,IT) is non empty Element of K32((G))
IT . () is set
(G,IT) is Element of K32((G))
IT . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 is non empty finite Element of K32((G))
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
K32((G,G1)) is non empty set
G2 is finite Element of K32((G,G1))
v2 is Relation-like NAT -defined Function-like finite () (G,G1,G2)
(G,v2) is non empty Element of K32((G))
v2 . () is set
(G,v2) is Element of K32((G))
v2 . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1}) /\ (G,{G1}) is Element of K32((G))
K32((G,{G1})) is non empty set
G2 is Element of K32((G,{G1}))
v2 is Relation-like NAT -defined Function-like finite () (G,{G1},G2)
(G,v2) is non empty Element of K32((G))
v2 . () is set
card (G,v2) is non empty V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1}) /\ (G,{G1}) is Element of K32((G))
K32((G,{G1})) is non empty set
v2 is Relation-like NAT -defined Function-like finite () (G,{G1}, {} )
G2 is finite Element of K32((G,{G1}))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 is non empty Element of K32((G))
G2 is Relation-like NAT -defined Function-like finite () (G,G1, {} )
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
K32((G,G1)) is non empty set
v2 is Element of K32((G,G1))
(G,G2) is Element of K32((G))
G2 . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
G2 is set
(G) . G1 is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
(G,(G)) is Element of K32((G))
K32((G)) is non empty set
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) /\ (G,(G)) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
e is set
(G) . e is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
K32((G)) is non empty set
(G) is non empty set
G . () is set
G1 is Element of K32((G))
G2 is Relation-like NAT -defined Function-like finite () (G,(G),G1)
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) /\ (G,(G)) is Element of K32((G))
(G,G2) is non empty Element of K32((G))
K32((G)) is non empty set
G2 . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G,(G), {} )
(G,(G)) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) /\ (G,(G)) is Element of K32((G))
(G,G1) is non empty Element of K32((G))
K32((G)) is non empty set
G1 . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G1 is set
{G1} is non empty trivial finite 1 -element set
(G) \ {G1} is Element of K32((G))
K32((G)) is non empty set
G2 is Relation-like NAT -defined Function-like finite () (G) (G,(G),(G) \ {G1})
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G1 is set
(G) \ G1 is Element of K32((G))
K32((G)) is non empty set
G2 is Relation-like NAT -defined Function-like finite () (G) (G,(G),(G) \ G1)
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1}) \/ (G,{G1}) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
G2 is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
G2 is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G2 is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G2 is set
G1 is Element of (G)
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
v2 is Element of (G)
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
card (G,G1) is V24() V25() V26() cardinal set
(G,G1) is Element of K32((G))
(G,{G1}) is Element of K32((G))
card (G,G1) is V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
card (G,G1) is V24() V25() V26() cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is Element of K32((G))
(G,{G1}) is Element of K32((G))
card (G,G1) is V24() V25() V26() cardinal set
(G,G1) +` (G,G1) is V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) +` (G,G1) is V24() V25() V26() cardinal set
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) + (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) +^ (G,G1) is V24() V25() V26() set
card ((G,G1) +^ (G,G1)) is V24() V25() V26() cardinal set
card ((G,G1) + (G,G1)) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G) .: (G,G1) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G,G1) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G) .: (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
K32((G)) is non empty set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G,G1) is Element of K32((G))
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
(G,{G1}) is Element of K32((G))
(G) .: (G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G,G1) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G) .: (G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) +` (G,G1) is V24() V25() V26() cardinal set
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) + (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) \/ (G,{G1}) is finite Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) +` (G,G1) is V24() V25() V26() cardinal set
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) + (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) \/ (G,{G1}) is finite Element of K32((G))
G2 is set
{G2} is non empty trivial finite 1 -element set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like finite set
K32(K33((G),(G))) is non empty finite V40() set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is set
{G2} is non empty trivial finite 1 -element set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like finite set
K32(K33((G),(G))) is non empty finite V40() set
G . () is set
(G) . G2 is set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is set
{G2} is non empty trivial finite 1 -element set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like finite set
K32(K33((G),(G))) is non empty finite V40() set
G . () is set
(G) . G2 is set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like V17( NAT ) set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is set
G1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G1 + 1) is set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is set
G1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G1 + 1) is set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . G1 is set
G1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G1 + 1) is set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . G2 is set
G2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G2 + 1) is set
G is Relation-like NAT -defined Function-like V17( NAT ) set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G) is set
the Relation-like NAT -defined Function-like finite () set is Relation-like NAT -defined Function-like finite () set
NAT --> the Relation-like NAT -defined Function-like finite () set is non empty Relation-like NAT -defined { the Relation-like NAT -defined Function-like finite () set } -valued Function-like constant V17( NAT ) V18( NAT ,{ the Relation-like NAT -defined Function-like finite () set }) V28() Function-yielding V48() Element of K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () set }))
{ the Relation-like NAT -defined Function-like finite () set } is non empty trivial functional finite V40() 1 -element set
K33(NAT,{ the Relation-like NAT -defined Function-like finite () set }) is non empty non trivial Relation-like non finite set
K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () set })) is non empty non trivial non finite set
dom (NAT --> the Relation-like NAT -defined Function-like finite () set ) is non empty V24() V25() V26() Element of K32(NAT)
G2 is Relation-like NAT -defined Function-like V17( NAT ) set
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G2 . v2 is set
rng G2 is set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like Function-like set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G . (G1 + 1) is Relation-like NAT -defined Function-like finite () set
the Relation-like NAT -defined Function-like finite () () () () () () () () set is Relation-like NAT -defined Function-like finite () () () () () () () () set
NAT --> the Relation-like NAT -defined Function-like finite () () () () () () () () set is non empty Relation-like NAT -defined { the Relation-like NAT -defined Function-like finite () () () () () () () () set } -valued Function-like constant V17( NAT ) V18( NAT ,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }) V28() Function-yielding V48() Element of K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }))
{ the Relation-like NAT -defined Function-like finite () () () () () () () () set } is non empty trivial functional finite V40() 1 -element set
K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }) is non empty non trivial Relation-like non finite set
K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set })) is non empty non trivial non finite set
dom (NAT --> the Relation-like NAT -defined Function-like finite () () () () () () () () set ) is non empty V24() V25() V26() Element of K32(NAT)
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G2 is Relation-like NAT -defined Function-like V17( NAT ) set
G2 . v2 is set
rng G2 is set
v2 is Relation-like NAT -defined Function-like V17( NAT ) () set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
v2 . (1 + 1) is Relation-like NAT -defined Function-like finite () set
rng v2 is set
v2 . 1 is Relation-like NAT -defined Function-like finite () set
e is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
v2 . e is Relation-like NAT -defined Function-like finite () set
the Relation-like NAT -defined Function-like finite () () () () () () () () set is Relation-like NAT -defined Function-like finite () () () () () () () () set
NAT --> the Relation-like NAT -defined Function-like finite () () () () () () () () set is non empty Relation-like NAT -defined { the Relation-like NAT -defined Function-like finite () () () () () () () () set } -valued Function-like constant V17( NAT ) V18( NAT ,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }) V28() Function-yielding V48() Element of K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }))
{ the Relation-like NAT -defined Function-like finite () () () () () () () () set } is non empty trivial functional finite V40() 1 -element set
K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set }) is non empty non trivial Relation-like non finite set
K32(K33(NAT,{ the Relation-like NAT -defined Function-like finite () () () () () () () () set })) is non empty non trivial non finite set
dom (NAT --> the Relation-like NAT -defined Function-like finite () () () () () () () () set ) is non empty V24() V25() V26() Element of K32(NAT)
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G2 is Relation-like NAT -defined Function-like V17( NAT ) set
G2 . v2 is set
rng G2 is set
v2 is Relation-like NAT -defined Function-like V17( NAT ) () set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
v2 . (1 + 1) is Relation-like NAT -defined Function-like finite () set
rng v2 is set
v2 . 1 is Relation-like NAT -defined Function-like finite () set
e is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
v2 . e is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () () set
G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () set
G is Relation-like NAT -defined Function-like V17( NAT ) () set
G1 is Relation-like NAT -defined Function-like V17( NAT ) () () () set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 . G2 is Relation-like NAT -defined Function-like finite () () () () set
G is Relation-like NAT -defined Function-like finite () set
dom G is finite Element of K32(NAT)
G1 is set
G is Relation-like NAT -defined Function-like finite set
(G) is set
G . () is set
G1 is Relation-like NAT -defined Function-like finite set
(G1) is set
G1 . () is set
G2 is Relation-like NAT -defined Function-like finite set
(G2) is set
G2 . () is set
v2 is Relation-like NAT -defined Function-like finite set
(v2) is set
v2 . () is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
dom (G) is Element of K32((G))
K32((G)) is non empty set
G1 is Relation-like NAT -defined Function-like finite () set
(G1) is set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
dom (G1) is Element of K32((G1))
K32((G1)) is non empty set
G2 is Relation-like NAT -defined Function-like finite () set
(G2) is non empty set
G2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
(G2) is set
G2 . () is set
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
rng (G2) is Element of K32((G2))
K32((G2)) is non empty set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is non empty set
v2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
(v2) is set
v2 . () is set
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
rng (v2) is Element of K32((v2))
K32((v2)) is non empty set
G is Relation-like NAT -defined Function-like finite set
dom G is finite Element of K32(NAT)
(G) is set
G . () is set
(G) is set
G . () is set
(G) is set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
(G) is set
G . () is set
G1 is Relation-like NAT -defined Function-like finite set
dom G1 is finite Element of K32(NAT)
(G1) is set
G1 . () is set
(G1) is set
G1 . () is set
(G1) is set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
(G1) is set
G1 . () is set
G1 is set
G is non empty set
K33(G1,G) is Relation-like set
K32(K33(G1,G)) is non empty set
v2 is set
e is non empty set
K33(v2,e) is Relation-like set
K32(K33(v2,e)) is non empty set
IT is set
S is non empty set
K33(IT,S) is Relation-like set
K32(K33(IT,S)) is non empty set
c₁₄ is set
c₁₃ is non empty set
K33(c₁₄,c₁₃) is Relation-like set
K32(K33(c₁₄,c₁₃)) is non empty set
G2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) Element of K32(K33(G1,G))
v2 is Relation-like G1 -defined G -valued Function-like V17(G1) V18(G1,G) Element of K32(K33(G1,G))
(G,G1,G2,v2) is Relation-like NAT -defined Function-like finite () set
<*G,G1,G2,v2*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((G,G1,G2,v2)) is non empty set
(G,G1,G2,v2) . () is set
Y is Relation-like v2 -defined e -valued Function-like V17(v2) V18(v2,e) Element of K32(K33(v2,e))
EV is Relation-like v2 -defined e -valued Function-like V17(v2) V18(v2,e) Element of K32(K33(v2,e))
(e,v2,Y,EV) is Relation-like NAT -defined Function-like finite () set
<*e,v2,Y,EV*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((e,v2,Y,EV)) is set
(e,v2,Y,EV) . () is set
IT is Relation-like IT -defined S -valued Function-like V17(IT) V18(IT,S) Element of K32(K33(IT,S))
IT is Relation-like IT -defined S -valued Function-like V17(IT) V18(IT,S) Element of K32(K33(IT,S))
(S,IT,IT,IT) is Relation-like NAT -defined Function-like finite () set
<*S,IT,IT,IT*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((S,IT,IT,IT)) is set
(S,IT,IT,IT) . () is set
((S,IT,IT,IT)) is non empty set
(S,IT,IT,IT) . () is set
((S,IT,IT,IT)) is Relation-like ((S,IT,IT,IT)) -defined ((S,IT,IT,IT)) -valued Function-like V17(((S,IT,IT,IT))) V18(((S,IT,IT,IT)),((S,IT,IT,IT))) Element of K32(K33(((S,IT,IT,IT)),((S,IT,IT,IT))))
K33(((S,IT,IT,IT)),((S,IT,IT,IT))) is Relation-like set
K32(K33(((S,IT,IT,IT)),((S,IT,IT,IT)))) is non empty set
(S,IT,IT,IT) . () is set
c₁₅ is Relation-like c₁₄ -defined c₁₃ -valued Function-like V17(c₁₄) V18(c₁₄,c₁₃) Element of K32(K33(c₁₄,c₁₃))
c₁₆ is Relation-like c₁₄ -defined c₁₃ -valued Function-like V17(c₁₄) V18(c₁₄,c₁₃) Element of K32(K33(c₁₄,c₁₃))
(c₁₃,c₁₄,c₁₅,c₁₆) is Relation-like NAT -defined Function-like finite () set
<*c₁₃,c₁₄,c₁₅,c₁₆*> is non empty Relation-like NAT -defined Function-like finite 4 -element FinSequence-like FinSubsequence-like set
((c₁₃,c₁₄,c₁₅,c₁₆)) is set
(c₁₃,c₁₄,c₁₅,c₁₆) . () is set
((c₁₃,c₁₄,c₁₅,c₁₆)) is non empty set
(c₁₃,c₁₄,c₁₅,c₁₆) . () is set
((c₁₃,c₁₄,c₁₅,c₁₆)) is Relation-like ((c₁₃,c₁₄,c₁₅,c₁₆)) -defined ((c₁₃,c₁₄,c₁₅,c₁₆)) -valued Function-like V17(((c₁₃,c₁₄,c₁₅,c₁₆))) V18(((c₁₃,c₁₄,c₁₅,c₁₆)),((c₁₃,c₁₄,c₁₅,c₁₆))) Element of K32(K33(((c₁₃,c₁₄,c₁₅,c₁₆)),((c₁₃,c₁₄,c₁₅,c₁₆))))
K33(((c₁₃,c₁₄,c₁₅,c₁₆)),((c₁₃,c₁₄,c₁₅,c₁₆))) is Relation-like set
K32(K33(((c₁₃,c₁₄,c₁₅,c₁₆)),((c₁₃,c₁₄,c₁₅,c₁₆)))) is non empty set
(c₁₃,c₁₄,c₁₅,c₁₆) . () is set
G is Relation-like NAT -defined Function-like finite set
dom G is finite Element of K32(NAT)
G1 is set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2,G1) is Relation-like NAT -defined Function-like finite set
G2 .--> G1 is Relation-like {G2} -defined Function-like one-to-one finite set
{G2} is non empty trivial finite V40() 1 -element set
{G2} --> G1 is non empty Relation-like {G2} -defined {G1} -valued Function-like constant V17({G2}) V18({G2},{G1}) finite Element of K32(K33({G2},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({G2},{G1}) is non empty Relation-like finite set
K32(K33({G2},{G1})) is non empty finite V40() set
G +* (G2 .--> G1) is Relation-like Function-like finite set
dom (G,G2,G1) is finite Element of K32(NAT)
(dom G) \/ {G2} is non empty finite set
dom (G2 .--> G1) is trivial finite V40() Element of K32({G2})
K32({G2}) is non empty finite V40() set
(dom G) \/ (dom (G2 .--> G1)) is finite set
G is Relation-like NAT -defined Function-like finite set
G1 is set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2,G1) is Relation-like NAT -defined Function-like finite set
G2 .--> G1 is Relation-like {G2} -defined Function-like one-to-one finite set
{G2} is non empty trivial finite V40() 1 -element set
{G2} --> G1 is non empty Relation-like {G2} -defined {G1} -valued Function-like constant V17({G2}) V18({G2},{G1}) finite Element of K32(K33({G2},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({G2},{G1}) is non empty Relation-like finite set
K32(K33({G2},{G1})) is non empty finite V40() set
G +* (G2 .--> G1) is Relation-like Function-like finite set
(G,G2,G1) . G2 is set
dom (G2 .--> G1) is trivial finite V40() Element of K32({G2})
K32({G2}) is non empty finite V40() set
(G2 .--> G1) . G2 is set
G is Relation-like NAT -defined Function-like finite set
G1 is set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2,G1) is Relation-like NAT -defined Function-like finite set
G2 .--> G1 is Relation-like {G2} -defined Function-like one-to-one finite set
{G2} is non empty trivial finite V40() 1 -element set
{G2} --> G1 is non empty Relation-like {G2} -defined {G1} -valued Function-like constant V17({G2}) V18({G2},{G1}) finite Element of K32(K33({G2},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({G2},{G1}) is non empty Relation-like finite set
K32(K33({G2},{G1})) is non empty finite V40() set
G +* (G2 .--> G1) is Relation-like Function-like finite set
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G . v2 is set
(G,G2,G1) . v2 is set
dom (G2 .--> G1) is trivial finite V40() Element of K32({G2})
K32({G2}) is non empty finite V40() set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
G2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2,G1) is Relation-like NAT -defined Function-like finite set
G2 .--> G1 is Relation-like {G2} -defined Function-like one-to-one finite set
{G2} is non empty trivial finite V40() 1 -element set
{G2} --> G1 is non empty Relation-like {G2} -defined {G1} -valued Function-like constant V17({G2}) V18({G2},{G1}) finite Element of K32(K33({G2},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({G2},{G1}) is non empty Relation-like finite set
K32(K33({G2},{G1})) is non empty finite V40() set
G +* (G2 .--> G1) is Relation-like Function-like finite set
((G,G2,G1)) is set
(G,G2,G1) . () is set
((G,G2,G1)) is set
(G,G2,G1) . () is set
((G,G2,G1)) is set
(G,G2,G1) . () is set
((G,G2,G1)) is set
(G,G2,G1) . () is set
dom G is finite Element of K32(NAT)
dom (G,G2,G1) is finite Element of K32(NAT)
dom (G2 .--> G1) is trivial finite V40() Element of K32({G2})
K32({G2}) is non empty finite V40() set
G is Relation-like NAT -defined Function-like finite set
G1 is set
(G,(),G1) is Relation-like NAT -defined Function-like finite set
() .--> G1 is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element set
{()} --> G1 is non empty Relation-like {()} -defined {G1} -valued Function-like constant V17({()}) V18({()},{G1}) finite Element of K32(K33({()},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({()},{G1}) is non empty Relation-like finite set
K32(K33({()},{G1})) is non empty finite V40() set
G +* (() .--> G1) is Relation-like Function-like finite set
((G,(),G1)) is set
(G,(),G1) . () is set
G2 is Relation-like NAT -defined Function-like finite set
v2 is set
(G2,(),v2) is Relation-like NAT -defined Function-like finite set
() .--> v2 is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element set
{()} --> v2 is non empty Relation-like {()} -defined {v2} -valued Function-like constant V17({()}) V18({()},{v2}) finite Element of K32(K33({()},{v2}))
{v2} is non empty trivial finite 1 -element set
K33({()},{v2}) is non empty Relation-like finite set
K32(K33({()},{v2})) is non empty finite V40() set
G2 +* (() .--> v2) is Relation-like Function-like finite set
((G2,(),v2)) is set
(G2,(),v2) . () is set
e is Relation-like NAT -defined Function-like finite set
v2 is set
(e,(),v2) is Relation-like NAT -defined Function-like finite set
() .--> v2 is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element set
{()} --> v2 is non empty Relation-like {()} -defined {v2} -valued Function-like constant V17({()}) V18({()},{v2}) finite Element of K32(K33({()},{v2}))
{v2} is non empty trivial finite 1 -element set
K33({()},{v2}) is non empty Relation-like finite set
K32(K33({()},{v2})) is non empty finite V40() set
e +* (() .--> v2) is Relation-like Function-like finite set
((e,(),v2)) is set
(e,(),v2) . () is set
Y is Relation-like NAT -defined Function-like finite set
EV is set
(Y,(),EV) is Relation-like NAT -defined Function-like finite set
() .--> EV is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element set
{()} --> EV is non empty Relation-like {()} -defined {EV} -valued Function-like constant V17({()}) V18({()},{EV}) finite Element of K32(K33({()},{EV}))
{EV} is non empty trivial finite 1 -element set
K33({()},{EV}) is non empty Relation-like finite set
K32(K33({()},{EV})) is non empty finite V40() set
Y +* (() .--> EV) is Relation-like Function-like finite set
((Y,(),EV)) is set
(Y,(),EV) . () is set
G is Relation-like NAT -defined Function-like finite set
G1 is set
G2 is set
v2 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,v2,G1) is Relation-like NAT -defined Function-like finite set
v2 .--> G1 is Relation-like {v2} -defined Function-like one-to-one finite set
{v2} is non empty trivial finite V40() 1 -element set
{v2} --> G1 is non empty Relation-like {v2} -defined {G1} -valued Function-like constant V17({v2}) V18({v2},{G1}) finite Element of K32(K33({v2},{G1}))
{G1} is non empty trivial finite 1 -element set
K33({v2},{G1}) is non empty Relation-like finite set
K32(K33({v2},{G1})) is non empty finite V40() set
G +* (v2 .--> G1) is Relation-like Function-like finite set
e is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
((G,v2,G1),e,G2) is Relation-like NAT -defined Function-like finite set
e .--> G2 is Relation-like {e} -defined Function-like one-to-one finite set
{e} is non empty trivial finite V40() 1 -element set
{e} --> G2 is non empty Relation-like {e} -defined {G2} -valued Function-like constant V17({e}) V18({e},{G2}) finite Element of K32(K33({e},{G2}))
{G2} is non empty trivial finite 1 -element set
K33({e},{G2}) is non empty Relation-like finite set
K32(K33({e},{G2})) is non empty finite V40() set
(G,v2,G1) +* (e .--> G2) is Relation-like Function-like finite set
dom ((G,v2,G1),e,G2) is finite Element of K32(NAT)
((G,v2,G1),e,G2) . v2 is set
((G,v2,G1),e,G2) . e is set
dom (G,v2,G1) is finite Element of K32(NAT)
(dom (G,v2,G1)) \/ {e} is non empty finite set
dom G is finite Element of K32(NAT)
(dom G) \/ {v2} is non empty finite set
(G,v2,G1) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is set
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is set
e is set
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G2 is set
v2 is set
G1 is set
e is Relation-like NAT -defined Function-like finite () set
Y is set
EV is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is set
e is set
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is set
G . () is set
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
G2 is set
G1 is set
(G) . G1 is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () () () set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) is V24() V25() V26() cardinal set
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) +` (G,G1) is V24() V25() V26() cardinal set
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) + (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) \/ (G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) /\ (G,G1) is finite Element of K32((G))
e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like finite set
K32(K33((G),(G))) is non empty finite V40() set
G . () is set
(G) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G) \ {G1} is Element of K32((G))
card (G) is non empty V24() V25() V26() cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty set
G . () is set
choose (G) is Element of (G)
G2 is Element of (G)
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G) \ {G2} is Element of K32((G))
((G) \ {G2}) \/ {G2} is non empty Element of K32((G))
card (((G) \ {G2}) \/ {G2}) is non empty V24() V25() V26() cardinal set
card ((G) \ {G2}) is V24() V25() V26() cardinal set
card {G2} is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(card ((G) \ {G2})) +` (card {G2}) is V24() V25() V26() cardinal set
0 +` 1 is V24() V25() V26() cardinal set
0 +^ 1 is V24() V25() V26() set
card (0 +^ 1) is V24() V25() V26() cardinal set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (0 + 1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty V24() V25() V26() cardinal set
e is non empty set
choose e is Element of e
Y is Element of (G)
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G1 is set
{G1} is non empty trivial finite 1 -element set
G2 is Element of (G)
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
G is Relation-like NAT -defined Function-like finite () () () () set
(G) is finite set
G . () is set
(G) is non empty finite set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like finite set
K32(K33((G),(G))) is non empty finite V40() set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) finite Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
v2 is set
e is set
G1 is set
G2 is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Relation-like NAT -defined Function-like finite () () set
(G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is non empty finite set
G1 . () is set
card (G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is set
{G1} is non empty trivial finite 1 -element set
G2 is Element of (G)
v2 is Element of (G)
{v2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
G2 is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
G1 is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
G2 is set
G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
(G,(G)) is Element of K32((G))
K32((G)) is non empty set
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) \/ (G,(G)) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
v2 is set
(G) . v2 is set
G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
e is set
v2 is Relation-like NAT -defined Function-like finite () set
v2 is set
(v2,v2) is Element of K32((v2))
(v2) is set
v2 . () is set
K32((v2)) is non empty set
(v2,v2) is Element of K32((v2))
(v2,v2) is Element of K32((v2))
(v2,v2) /\ (v2,v2) is Element of K32((v2))
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
(v2) is non empty set
v2 . () is set
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
(v2) . e is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
v2 . () is set
(v2) . e is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
v2 is set
e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
(G,(G)) is Element of K32((G))
K32((G)) is non empty set
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) /\ (G,(G)) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
e is set
(G) . e is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
G1 is set
(G,G1) is Element of K32((G))
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
(G) \ (G,G1) is Element of K32((G))
(G) \ G1 is Element of K32((G))
K32((G)) is non empty set
(G,((G) \ G1)) is Element of K32((G))
(G,((G) \ G1)) is Element of K32((G))
(G,((G) \ G1)) is Element of K32((G))
(G,((G) \ G1)) /\ (G,((G) \ G1)) is Element of K32((G))
Y is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . Y is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . Y is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
G2 is set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is set
e is set
(G,G1,v2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2,e) is Element of K32((G))
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is set
e is set
(G,G1,v2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2,e) is Element of K32((G))
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G,(G),{G1}) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1},(G)) is Element of K32((G))
G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G2 is set
G2 is set
(G) . G2 is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is Relation-like NAT -defined Function-like finite () set
(G1) is non empty set
G1 . () is set
(G1) is set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
dom (G) is Element of K32((G))
K32((G)) is non empty set
dom (G1) is Element of K32((G1))
K32((G1)) is non empty set
G2 is set
(G) . G2 is set
(G1) . G2 is set
dom (G) is Element of K32((G))
dom (G1) is Element of K32((G1))
G2 is set
(G) . G2 is set
(G1) . G2 is set
G2 is set
(G) . G2 is set
(G1) . G2 is set
(G) . G2 is set
(G1) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
v2 is Relation-like NAT -defined Function-like finite () set
G2 is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 . () is set
v2 is set
e is Relation-like NAT -defined Function-like finite () (v2)
(v2,e) is Element of K32((v2))
(v2) is set
v2 . () is set
K32((v2)) is non empty set
e . () is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is Relation-like NAT -defined Function-like finite () (G1)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G1,G2) is non empty Element of K32((G1))
(G1) is non empty set
G1 . () is set
K32((G1)) is non empty set
G2 . () is set
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G1,G2) is Element of K32((G1))
(G1) is set
K32((G1)) is non empty set
G2 . () is set
v2 is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
(G2) is set
(G2) is non empty set
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(G2) . v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
(G2) . v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 . () is set
G2 is Relation-like NAT -defined Function-like finite () (G)
(G,G2) is non empty Element of K32((G))
G2 . () is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
(G2) is set
(G2) is non empty set
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(G2) . v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
(G2) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
G1 . () is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G,G1) is Element of K32((G))
K32((G)) is non empty set
(G) | (G,G1) is Relation-like (G) -defined (G,G1) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G) | (G,G1) is Relation-like (G) -defined (G,G1) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
e is set
dom (G1) is Element of K32((G1))
K32((G1)) is non empty set
(G1) . e is set
(G) . e is set
((G) | (G,G1)) . e is set
dom (G) is Element of K32((G))
dom ((G) | (G,G1)) is Element of K32((G))
e is set
dom (G1) is Element of K32((G1))
(G1) . e is set
(G) . e is set
((G) | (G,G1)) . e is set
dom (G) is Element of K32((G))
dom ((G) | (G,G1)) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 is set
v2 is set
G2 is set
e is set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
v2 is Relation-like NAT -defined Function-like finite () (G,G1,v2)
Y is Relation-like NAT -defined Function-like finite () (G,G2,e)
(G,Y) is non empty Element of K32((G))
Y . () is set
(G,Y) is Element of K32((G))
Y . () is set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G,v2) is non empty Element of K32((G))
v2 . () is set
(G,v2) is Element of K32((G))
v2 . () is set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G,v2) is non empty Element of K32((G))
v2 . () is set
(G,v2) is Element of K32((G))
v2 . () is set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty set
G . () is set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element set
(G) \ {G1} is Element of K32((G))
K32((G)) is non empty set
(G,((G) \ {G1})) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,((G) \ {G1})) is Element of K32((G))
(G,((G) \ {G1})) is Element of K32((G))
(G,((G) \ {G1})) /\ (G,((G) \ {G1})) is Element of K32((G))
{G1} is non empty trivial finite 1 -element Element of K32((G))
(G) \ {G1} is Element of K32((G))
(G,((G) \ {G1})) is Element of K32((G))
(G,((G) \ {G1})) is Element of K32((G))
(G,((G) \ {G1})) is Element of K32((G))
(G,((G) \ {G1})) /\ (G,((G) \ {G1})) is Element of K32((G))
G2 is Relation-like NAT -defined Function-like finite () (G,(G) \ {G1},(G,((G) \ {G1})))
(G,G2) is non empty Element of K32((G))
G2 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
card (G) is non empty V24() V25() V26() cardinal set
v2 is non empty Element of K32((G))
(G,v2) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,v2) /\ (G,v2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () () () set
(G) is non empty finite set
G . () is set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is finite set
G . () is set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Element of (G)
{G1} is non empty trivial finite 1 -element set
(G) \ {G1} is finite Element of K32((G))
K32((G)) is non empty finite V40() set
(G,((G) \ {G1})) is finite Element of K32((G))
K32((G)) is non empty finite V40() set
(G,((G) \ {G1})) is finite Element of K32((G))
(G,((G) \ {G1})) is finite Element of K32((G))
(G,((G) \ {G1})) /\ (G,((G) \ {G1})) is finite Element of K32((G))
(G,G1) is finite Element of K32((G))
{G1} is non empty trivial finite 1 -element Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) is finite Element of K32((G))
(G,{G1}) \/ (G,{G1}) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is Relation-like NAT -defined Function-like finite () () (G,(G) \ {G1},(G,((G) \ {G1})))
(G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is non empty finite set
G2 . () is set
card (G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is finite set
G2 . () is set
card (G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + (card (G,G1)) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is non empty finite Element of K32((G))
(G,G2) is finite Element of K32((G))
(G) \ {G1} is finite Element of K32((G))
((G) \ {G1}) \/ {G1} is non empty finite Element of K32((G))
card (((G) \ {G1}) \/ {G1}) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,((G) \ {G1})) is finite Element of K32((G))
(G,((G) \ {G1})) is finite Element of K32((G))
(G,((G) \ {G1})) is finite Element of K32((G))
(G,((G) \ {G1})) /\ (G,((G) \ {G1})) is finite Element of K32((G))
(G) \ (G,G1) is finite Element of K32((G))
(G,G2) \/ (G,G1) is finite Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
(G) \ G1 is Element of K32((G))
K32((G)) is non empty set
(G,((G) \ G1)) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,((G) \ G1)) is Element of K32((G))
(G,((G) \ G1)) is Element of K32((G))
(G,((G) \ G1)) /\ (G,((G) \ G1)) is Element of K32((G))
G2 is Relation-like NAT -defined Function-like finite () (G,(G) \ G1,(G,((G) \ G1)))
(G,G2) is non empty Element of K32((G))
G2 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
e is non empty Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) /\ (G,e) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
K32((G)) is non empty finite V40() set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is finite set
G . () is set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is finite Element of K32((G))
(G) \ G1 is finite Element of K32((G))
(G,((G) \ G1)) is finite Element of K32((G))
K32((G)) is non empty finite V40() set
(G,((G) \ G1)) is finite Element of K32((G))
(G,((G) \ G1)) is finite Element of K32((G))
(G,((G) \ G1)) /\ (G,((G) \ G1)) is finite Element of K32((G))
card G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
(G,G1) is finite Element of K32((G))
(G,G1) is finite Element of K32((G))
(G,G1) \/ (G,G1) is finite Element of K32((G))
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is Relation-like NAT -defined Function-like finite () () (G,(G) \ G1,(G,((G) \ G1)))
(G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is non empty finite set
G2 . () is set
card (G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + (card G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is finite set
G2 . () is set
card (G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + (card (G,G1)) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is non empty finite Element of K32((G))
(G,G2) is finite Element of K32((G))
(G) \ (G,G1) is finite Element of K32((G))
(G,G2) \/ G1 is non empty finite Element of K32((G))
card ((G,G2) \/ G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G,G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(card (G,G2)) + (card G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) \/ (G,G1) is finite Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G1 is set
{G1} is non empty trivial finite 1 -element set
(G) \ {G1} is Element of K32((G))
K32((G)) is non empty set
G2 is Relation-like NAT -defined Function-like finite () (G) (G,(G),(G) \ {G1})
(G,G2) is non empty Element of K32((G))
K32((G)) is non empty set
G2 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
e is non empty Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) /\ (G,e) is Element of K32((G))
K32((G,e)) is non empty set
Y is Element of K32((G,e))
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
(G) is finite set
G . () is set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is set
{G1} is non empty trivial finite 1 -element set
(G) \ {G1} is finite Element of K32((G))
K32((G)) is non empty finite V40() set
G2 is Relation-like NAT -defined Function-like finite () () (G) (G,(G),(G) \ {G1})
(G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is non empty finite set
G2 . () is set
card (G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is finite set
G2 . () is set
card (G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is finite Element of K32((G))
v2 is set
(G,G2) \/ {G1} is non empty finite set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G1 is set
(G) \ G1 is Element of K32((G))
K32((G)) is non empty set
G2 is Relation-like NAT -defined Function-like finite () (G) (G,(G),(G) \ G1)
(G,G2) is non empty Element of K32((G))
K32((G)) is non empty set
G2 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
e is non empty Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) is Element of K32((G))
(G,e) /\ (G,e) is Element of K32((G))
K32((G,e)) is non empty set
Y is Element of K32((G,e))
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
(G) is finite set
G . () is set
G1 is set
(G) \ G1 is finite Element of K32((G))
K32((G)) is non empty finite V40() set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G2 is Relation-like NAT -defined Function-like finite () () (G) (G,(G),(G) \ G1)
(G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is non empty finite set
G2 . () is set
card (G2) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G is Relation-like NAT -defined Function-like finite () () set
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
(G) is non empty finite set
G . () is set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is finite Element of K32((G))
(G) \ G1 is finite Element of K32((G))
card G1 is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G2 is Relation-like NAT -defined Function-like finite () () (G) (G,(G),(G) \ G1)
(G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G2) is finite set
G2 . () is set
card (G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G2) + (card G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is finite Element of K32((G))
(G,G2) \/ G1 is finite Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is non empty set
v2 . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
e is set
(v2) is set
v2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
(v2) . e is set
v2 is Element of (v2)
(v2,v2) is Element of K32((v2))
K32((v2)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((v2))
K32((v2)) is non empty set
(v2,{v2}) is Element of K32((v2))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
e is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
v2 is Relation-like NAT -defined Function-like finite () set
(v2) is non empty set
v2 . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
e is set
(v2) is set
v2 . () is set
(v2) is Relation-like (v2) -defined (v2) -valued Function-like V17((v2)) V18((v2),(v2)) Element of K32(K33((v2),(v2)))
K33((v2),(v2)) is Relation-like set
K32(K33((v2),(v2))) is non empty set
v2 . () is set
(v2) . e is set
v2 is Element of (v2)
(v2,v2) is Element of K32((v2))
K32((v2)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((v2))
K32((v2)) is non empty set
(v2,{v2}) is Element of K32((v2))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
e is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Element of (G)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G1} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G1}) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1}) is Element of K32((G))
(G,{G1}) \/ (G,{G1}) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) \/ (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
G1 is set
(G) . G1 is set
(G) . G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is set
v2 is Element of (G)
(G,v2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{v2}) is Element of K32((G))
(G,{v2}) is Element of K32((G))
(G,{v2}) is Element of K32((G))
(G,{v2}) \/ (G,{v2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
v2 is Element of (G)
(G,v2) is Element of K32((G))
{v2} is non empty trivial finite 1 -element Element of K32((G))
(G,{v2}) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,{v2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
e is Element of (G)
v2 is Element of (G)
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
e is Element of (G)
v2 is Element of (G)
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
v2 is Element of (G)
v2 is Element of (G)
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is set
v2 is set
e is Element of (G)
(G,e) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{e} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{e}) is Element of K32((G))
(G,{e}) is Element of K32((G))
(G,{e}) is Element of K32((G))
(G,{e}) \/ (G,{e}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2,G1) is Element of (G)
v2 is Element of (G)
(G,v2,G1) is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G,G2,G1) is Element of (G)
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . G1 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . G1 is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is set
G2 is Element of (G)
v2 is Element of (G)
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is V24() V25() V26() cardinal set
(G,G2) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G2}) is finite Element of K32((G))
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2) is V24() V25() V26() cardinal set
(G,G2) is finite Element of K32((G))
(G,{G2}) is finite Element of K32((G))
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2) +` (G,G2) is V24() V25() V26() cardinal set
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) + (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,v2) is V24() V25() V26() cardinal set
(G,v2) is finite Element of K32((G))
{v2} is non empty trivial finite 1 -element Element of K32((G))
(G,{v2}) is finite Element of K32((G))
card (G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,v2) is V24() V25() V26() cardinal set
(G,v2) is finite Element of K32((G))
(G,{v2}) is finite Element of K32((G))
card (G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,v2) +` (G,v2) is V24() V25() V26() cardinal set
(G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,v2) + (G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
{G1} is non empty trivial finite 1 -element set
e is set
card {G1} is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
e is set
card (G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
{G1} is non empty trivial finite 1 -element set
e is set
card {G1} is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
e is set
card (G,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
dom (G) is Element of K32((G))
v2 is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
e is set
(G) . e is set
v2 is set
(G) . v2 is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
dom (G) is Element of K32((G))
v2 is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
e is set
(G) . e is set
v2 is set
(G) . v2 is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
v2 is set
e is set
v2 is set
e is set
v2 is set
v2 is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is set
v2 is set
e is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
e is set
G2 is set
v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
(G) | (G,G1) is Relation-like (G,G1) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
((G) | (G,G1)) . e is set
(G) | (G,G1) is Relation-like (G,G1) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
((G) | (G,G1)) . e is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G) (G)
G2 is Relation-like NAT -defined Function-like finite () (G1) (G1)
(G1,G2) is non empty Element of K32((G1))
(G1) is non empty set
G1 . () is set
K32((G1)) is non empty set
G2 . () is set
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is non empty finite set
G . () is set
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G) is finite set
G . () is set
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
G1 is Relation-like NAT -defined Function-like finite () () (G)
(G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is non empty finite set
G1 . () is set
card (G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1) is finite set
G1 . () is set
card (G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G1) is non empty finite Element of K32((G))
K32((G)) is non empty finite V40() set
card (G,G1) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is non empty ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
K32((G)) is non empty finite V40() set
card (G,G1) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
card (G) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is set
(G1,G2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G1,G2) is Element of K32((G1))
(G,G2) is Element of K32((G))
(G1,G2) is Element of K32((G1))
(G1,G2) \/ (G1,G2) is Element of K32((G1))
(G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
(G1,G2) is Element of K32((G1))
(G1,G2) /\ (G1,G2) is Element of K32((G1))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
(G) is non empty set
G . () is set
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G,G1) is Element of K32((G))
v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is set
v2 is set
(G1,G2,v2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
(G,G2,v2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G1,G2,v2) is Element of K32((G1))
(G,G2,v2) is Element of K32((G))
e is set
e is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
v2 is Element of (G1)
(G1,v2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{v2}) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) \/ (G1,{v2}) is Element of K32((G1))
e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G,G1) is Element of K32((G))
e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
e is set
(G1) . e is set
(G1) . e is set
(G) . e is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G) is set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
(G,G1) is Element of K32((G))
K32((G)) is non empty set
G1 . () is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,G2) /\ (G,G1) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,G2) /\ (G,G1) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G,G2) /\ (G,G1) is Element of K32((G))
v2 is Element of (G1)
(G1,v2) is Element of K32((G1))
(G1) is set
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{v2}) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) \/ (G1,{v2}) is Element of K32((G1))
e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
e is set
(G,G2) \/ (G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
G2 is Element of (G)
v2 is Element of (G1)
e is set
(G,G2,e) is Element of (G)
(G1,v2,e) is Element of (G1)
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . e is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . e is set
G is Relation-like NAT -defined Function-like finite () () set
(G) is non empty finite set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () () (G)
(G1) is non empty finite set
G1 . () is set
G2 is Element of (G)
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is finite Element of K32((G))
(G) is finite set
G . () is set
K32((G)) is non empty finite V40() set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty finite V40() set
(G,{G2}) is finite Element of K32((G))
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is finite Element of K32((G))
(G,{G2}) is finite Element of K32((G))
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G2) is V24() V25() V26() cardinal set
(G,G2) is V24() V25() V26() cardinal set
(G,G2) +` (G,G2) is V24() V25() V26() cardinal set
(G,G2) + (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
v2 is Element of (G1)
(G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1,v2) is finite Element of K32((G1))
(G1) is finite set
G1 . () is set
K32((G1)) is non empty finite V40() set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty finite V40() set
(G1,{v2}) is finite Element of K32((G1))
card (G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1,v2) is finite Element of K32((G1))
(G1,{v2}) is finite Element of K32((G1))
card (G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal set
(G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G1,v2) is V24() V25() V26() cardinal set
(G1,v2) is V24() V25() V26() cardinal set
(G1,v2) +` (G1,v2) is V24() V25() V26() cardinal set
(G1,v2) + (G1,v2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
(G,G1) is finite Element of K32((G))
(G,G2) /\ (G,G1) is finite Element of K32((G))
(G,G2) /\ (G,G1) is finite Element of K32((G))
card (G,G2) is ext-real non negative V24() V25() V26() V30() V31() V32() finite cardinal Element of NAT
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
G2 is Element of (G)
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G) is set
G . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G,G2) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G) .: (G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
v2 is Element of (G1)
(G1,v2) is Element of K32((G1))
K32((G1)) is non empty set
(G1) is set
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1,v2) is Element of K32((G1))
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1) .: (G1,v2) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1,v2) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1) .: (G1,v2) is Element of K32((G1))
(G1,v2) is Element of K32((G1))
(G1,v2) \/ (G1,v2) is Element of K32((G1))
e is set
v2 is set
e is set
v2 is set
e is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
G2 is Element of (G)
v2 is Element of (G1)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G1,v2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) \/ (G1,{v2}) is Element of K32((G1))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G1) is non empty set
G1 . () is set
G2 is Element of (G)
v2 is Element of (G1)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
e is set
{e} is non empty trivial finite 1 -element set
(G1,v2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) \/ (G1,{v2}) is Element of K32((G1))
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G) is non empty set
G . () is set
(G1) is set
G1 . () is set
(G1) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G2) is set
G2 . () is set
(G2) is non empty set
G2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 . () is set
G2 is Relation-like NAT -defined Function-like finite () (G)
(G,G2) is non empty Element of K32((G))
G2 . () is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
(G1) is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is non empty set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
dom (G1) is Element of K32((G1))
K32((G1)) is non empty set
(G2) is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
(G2) is non empty set
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
dom (G2) is Element of K32((G2))
K32((G2)) is non empty set
v2 is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G2) . v2 is set
v2 is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
(G2) . v2 is set
dom (G1) is Element of K32((G1))
dom (G2) is Element of K32((G2))
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G1) is non empty set
G1 . () is set
(G) is set
G . () is set
(G1) is set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
G2 is set
v2 is set
e is set
v2 is set
Y is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G1) is set
G1 . () is set
(G) is non empty set
G . () is set
(G1) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
G2 is set
(G1) . G2 is set
(G1) . G2 is set
card (G1) is non empty V24() V25() V26() cardinal set
e is set
v2 is set
G2 is set
v2 is set
e is set
v2 is set
G2 is set
v2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is V24() V25() V26() cardinal set
(G) is non empty set
G . () is set
card (G) is non empty V24() V25() V26() cardinal set
(G) is V24() V25() V26() cardinal set
(G) is set
G . () is set
card (G) is V24() V25() V26() cardinal set
G1 is Relation-like NAT -defined Function-like finite () set
(G1) is V24() V25() V26() cardinal set
(G1) is non empty set
G1 . () is set
card (G1) is non empty V24() V25() V26() cardinal set
(G1) is V24() V25() V26() cardinal set
(G1) is set
G1 . () is set
card (G1) is V24() V25() V26() cardinal set
G2 is set
(G,G2) is Element of K32((G))
K32((G)) is non empty set
(G1,G2) is Element of K32((G1))
K32((G1)) is non empty set
(G,G2) is Element of K32((G))
(G1,G2) is Element of K32((G1))
(G,G2) is Element of K32((G))
(G,G2) \/ (G,G2) is Element of K32((G))
(G1,G2) is Element of K32((G1))
(G1,G2) \/ (G1,G2) is Element of K32((G1))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
(G1,G2) is Element of K32((G1))
(G1,G2) /\ (G1,G2) is Element of K32((G1))
v2 is set
(G,G2,v2) is Element of K32((G))
(G1,G2,v2) is Element of K32((G1))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
e is set
(G1) . e is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
e is set
(G1) . e is set
e is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
(G2) is non empty set
G2 . () is set
(G) is non empty set
G . () is set
(G1) is non empty set
G1 . () is set
(G2) is set
G2 . () is set
(G1) is set
G1 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G) is set
G . () is set
v2 is set
(G2) . v2 is set
(G1) . v2 is set
(G2) . v2 is set
(G1) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) . v2 is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
G2 is Relation-like NAT -defined Function-like finite () set
(G) is set
G . () is set
(G1) is set
G1 . () is set
(G) is non empty set
G . () is set
(G1) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G2) is non empty set
G2 . () is set
(G2) is set
G2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
K33((G2),(G2)) is Relation-like set
K32(K33((G2),(G2))) is non empty set
G2 . () is set
(G2) is Relation-like (G2) -defined (G2) -valued Function-like V17((G2)) V18((G2),(G2)) Element of K32(K33((G2),(G2)))
G2 . () is set
v2 is set
(G1) . v2 is set
(G2) . v2 is set
(G1) . v2 is set
(G2) . v2 is set
G is Relation-like NAT -defined Function-like finite () set
G1 is set
G2 is set
v2 is Relation-like NAT -defined Function-like finite () (G,G1,G2)
e is Relation-like NAT -defined Function-like finite () (G,G1,G2)
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G,v2) is Element of K32((G))
v2 . () is set
(G,e) is Element of K32((G))
e . () is set
(G,v2) is non empty Element of K32((G))
v2 . () is set
(G,e) is non empty Element of K32((G))
e . () is set
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G1) is Element of K32((G))
(G,G1) is Element of K32((G))
(G,G1) /\ (G,G1) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
(G,(G)) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,(G)) is Element of K32((G))
(G,(G)) is Element of K32((G))
(G,(G)) /\ (G,(G)) is Element of K32((G))
G1 is Relation-like NAT -defined Function-like finite () (G) (G,(G),(G,(G)))
(G,G1) is Element of K32((G))
G1 . () is set
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
(G1) is set
(G1) is non empty set
G1 . () is set
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) | (G) is Relation-like (G) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
dom (G) is Element of K32((G))
(G) | (dom (G)) is Relation-like (G) -defined dom (G) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) | (G) is Relation-like (G) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
dom (G) is Element of K32((G))
(G) | (dom (G)) is Relation-like (G) -defined dom (G) -defined (G) -defined (G) -valued Function-like Element of K32(K33((G),(G)))
(G,G1) is non empty Element of K32((G))
K32((G)) is non empty set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () set
G2 is set
v2 is set
e is Relation-like NAT -defined Function-like finite () (G,G2,v2)
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
(G,e) is non empty Element of K32((G))
e . () is set
(G,e) is Element of K32((G))
e . () is set
(G1) is non empty set
G1 . () is set
K32((G1)) is non empty set
(G1,G2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
(G1,G2) is Element of K32((G1))
(G1,G2) is Element of K32((G1))
(G1,G2) /\ (G1,G2) is Element of K32((G1))
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
(G1) is non empty set
G1 . () is set
K32((G1)) is non empty set
(G1,G2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
(G1,G2) is Element of K32((G1))
(G1,G2) is Element of K32((G1))
(G1,G2) /\ (G1,G2) is Element of K32((G1))
(G) is non empty set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
(G,G2) is Element of K32((G))
(G,G2) is Element of K32((G))
(G,G2) /\ (G,G2) is Element of K32((G))
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () set
(G1) is non empty set
G1 . () is set
G2 is set
v2 is Element of (G)
(G,v2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{v2}) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,{v2}) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,{v2}) is Element of K32((G))
(G,{v2}) \/ (G,{v2}) is Element of K32((G))
(G,v2,G2) is Element of (G)
(G,v2) is V24() V25() V26() cardinal set
card (G,v2) is V24() V25() V26() cardinal set
(G,v2) is V24() V25() V26() cardinal set
card (G,v2) is V24() V25() V26() cardinal set
(G,v2) is V24() V25() V26() cardinal set
(G,v2) +` (G,v2) is V24() V25() V26() cardinal set
(G,v2) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
K33((G),(G)) is Relation-like set
K32(K33((G),(G))) is non empty set
G . () is set
(G) .: (G,v2) is Element of K32((G))
(G,v2) is Element of K32((G))
(G) is Relation-like (G) -defined (G) -valued Function-like V17((G)) V18((G),(G)) Element of K32(K33((G),(G)))
G . () is set
(G) .: (G,v2) is Element of K32((G))
(G,v2) is Element of K32((G))
(G,v2) \/ (G,v2) is Element of K32((G))
e is Element of (G1)
(G1,e) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
{e} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{e}) is Element of K32((G1))
(G1,e) is Element of K32((G1))
(G1,{e}) is Element of K32((G1))
(G1,e) is Element of K32((G1))
(G1,{e}) is Element of K32((G1))
(G1,{e}) \/ (G1,{e}) is Element of K32((G1))
(G1,e,G2) is Element of (G1)
(G1,e) is V24() V25() V26() cardinal set
card (G1,e) is V24() V25() V26() cardinal set
(G1,e) is V24() V25() V26() cardinal set
card (G1,e) is V24() V25() V26() cardinal set
(G1,e) is V24() V25() V26() cardinal set
(G1,e) +` (G1,e) is V24() V25() V26() cardinal set
(G1,e) is Element of K32((G1))
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
K33((G1),(G1)) is Relation-like set
K32(K33((G1),(G1))) is non empty set
G1 . () is set
(G1) .: (G1,e) is Element of K32((G1))
(G1,e) is Element of K32((G1))
(G1) is Relation-like (G1) -defined (G1) -valued Function-like V17((G1)) V18((G1),(G1)) Element of K32(K33((G1),(G1)))
G1 . () is set
(G1) .: (G1,e) is Element of K32((G1))
(G1,e) is Element of K32((G1))
(G1,e) \/ (G1,e) is Element of K32((G1))
(G) . G2 is set
(G1) . G2 is set
(G) . G2 is set
(G1) . G2 is set
(G) . G2 is set
(G) . G2 is set
(G1) . G2 is set
(G1) . G2 is set
(G) . G2 is set
(G) . G2 is set
(G1) . G2 is set
(G1) . G2 is set
(G) . G2 is set
(G) . G2 is set
G is Relation-like NAT -defined Function-like finite () set
(G) is non empty set
G . () is set
G1 is Relation-like NAT -defined Function-like finite () set
(G1) is non empty set
G1 . () is set
G2 is Element of (G)
v2 is Element of (G1)
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
{G2} is non empty trivial finite 1 -element Element of K32((G))
K32((G)) is non empty set
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) is Element of K32((G))
(G,{G2}) \/ (G,{G2}) is Element of K32((G))
(G1,v2) is Element of K32((G1))
(G1) is set
G1 . () is set
K32((G1)) is non empty set
{v2} is non empty trivial finite 1 -element Element of K32((G1))
K32((G1)) is non empty set
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) is Element of K32((G1))
(G1,{v2}) \/ (G1,{v2}) is Element of K32((G1))
e is set
{e} is non empty trivial finite 1 -element set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is Relation-like NAT -defined Function-like finite () (G)
(G,G1) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G,G2) is non empty Element of K32((G))
G2 . () is set
(G,G1) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G1 . () is set
(G,G2) is Element of K32((G))
G2 . () is set
G is Relation-like NAT -defined Function-like finite () set
G1 is Relation-like NAT -defined Function-like finite () (G)
G2 is Relation-like NAT -defined Function-like finite () (G)
(G,G2) is non empty Element of K32((G))
(G) is non empty set
G . () is set
K32((G)) is non empty set
G2 . () is set
(G,G1) is non empty Element of K32((G))
G1 . () is set
(G,G2) is Element of K32((G))
(G) is set
G . () is set
K32((G)) is non empty set
G2 . () is set
(G,G1) is Element of K32((G))
G1 . () is set