:: 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