:: ZF_FUND2 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal limit_cardinal Element of bool REAL

bool REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal limit_cardinal set

bool NAT is non trivial V35() set

bool NAT is non trivial V35() set

VAR is non empty Element of bool NAT

bool VAR is set

[:NAT,VAR:] is non trivial V35() set

bool [:NAT,VAR:] is non trivial V35() set

{} is set

the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V28() V29() V35() V39() cardinal {} -element set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V28() V29() V35() V39() cardinal {} -element set

1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal set

the_axiom_of_pairs is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

the_axiom_of_unions is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

the_axiom_of_infinity is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

the_axiom_of_power_sets is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

x. 0 is Element of VAR

x. 1 is Element of VAR

2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

x. 2 is Element of VAR

{(x. 0),(x. 1),(x. 2)} is V35() set

3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

x. 3 is Element of VAR

4 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

x. 4 is Element of VAR

(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

decode is Relation-like NAT -defined VAR -valued Function-like quasi_total Element of bool [:NAT,VAR:]

decode " is Relation-like Function-like set

L is non empty set

[:VAR,L:] is set

bool [:VAR,L:] is set

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free W is V35() Element of bool VAR

ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

{ b

bool L is set

l is set

u is Element of L

ksi / ((x. 0),u) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(x. 2) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

(x. 2) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

W is non empty set

[:VAR,W:] is set

bool [:VAR,W:] is set

L is Element of W

bool L is set

W /\ (bool L) is set

ksi is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

ksi / ((x. 1),L) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),W,(ksi / ((x. 1),L))) is Element of bool W

bool W is set

Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) is V35() Element of bool VAR

Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))) is V35() Element of bool VAR

{(x. 2)} is non empty trivial V35() 1 -element set

(Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)} is V35() Element of bool VAR

Free ((x. 2) 'in' (x. 0)) is V35() Element of bool VAR

Free ((x. 2) 'in' (x. 1)) is V35() Element of bool VAR

(Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1))) is V35() Element of bool VAR

((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} is V35() Element of bool VAR

{(x. 2),(x. 1)} is V35() set

(Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)} is V35() set

((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)})

bool ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) is V35() V39() set

{(x. 2),(x. 0)} is V35() set

{(x. 2),(x. 0)} \/ {(x. 2),(x. 1)} is V35() set

({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)})

bool ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) is V35() V39() set

{(x. 2),(x. 0)} \ {(x. 2)} is V35() Element of bool {(x. 2),(x. 0)}

bool {(x. 2),(x. 0)} is V35() V39() set

{(x. 2),(x. 1)} \ {(x. 2)} is V35() Element of bool {(x. 2),(x. 1)}

bool {(x. 2),(x. 1)} is V35() V39() set

({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) is V35() set

{(x. 1)} is non empty trivial V35() 1 -element set

({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)} is V35() set

{(x. 0)} is non empty trivial V35() 1 -element set

{(x. 0)} \/ {(x. 1)} is V35() set

{(x. 0),(x. 1)} is V35() set

{ b

u1 is set

u2 is Element of W

(ksi / ((x. 1),L)) / ((x. 0),u2) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

i is set

a is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 2) is Element of W

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 1) is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 1) is Element of W

(ksi / ((x. 1),L)) . (x. 1) is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 0) is Element of W

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 0) is Element of W

u1 is set

(ksi / ((x. 1),L)) . (x. 1) is Element of W

u2 is Element of W

(ksi / ((x. 1),L)) / ((x. 0),u2) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

i is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 2) is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 0) is Element of W

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 0) is Element of W

(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 1) is Element of W

((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 1) is Element of W

W is Relation-like Function-like set

Union W is set

dom W is set

L is set

rng W is set

union (rng W) is set

ksi is set

lambda is set

W . lambda is set

W is non empty epsilon-transitive V33() V34() universal set

L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set

Union L is non empty Element of bool W

bool W is set

lambda is set

bool lambda is set

l is epsilon-transitive epsilon-connected ordinal Element of W

L . l is non empty Element of W

(L . l) /\ (bool lambda) is set

[:VAR,(L . l):] is set

bool [:VAR,(L . l):] is set

the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] is Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):]

u1 is Element of L . l

the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] / ((x. 1),u1) is Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):]

((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(L . l),( the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] / ((x. 1),u1))) is Element of bool (L . l)

bool (L . l) is set

lambda is set

bool lambda is set

(Union L) /\ (bool lambda) is Element of bool W

l is non empty set

u is Element of l

dom L is epsilon-transitive epsilon-connected ordinal set

u1 is set

L . u1 is set

On W is non empty epsilon-transitive epsilon-connected ordinal set

u2 is epsilon-transitive epsilon-connected ordinal Element of W

L . u2 is set

u is Relation-like Function-like set

dom u is set

rng u is set

u1 is set

u2 is set

u . u2 is set

i is Element of l

u . i is set

a is epsilon-transitive epsilon-connected ordinal Element of W

L . a is non empty Element of W

u .: (dom u) is set

card l is non empty epsilon-transitive epsilon-connected ordinal cardinal set

card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set

card (rng u) is epsilon-transitive epsilon-connected ordinal cardinal set

sup (rng u) is epsilon-transitive epsilon-connected ordinal set

u1 is epsilon-transitive epsilon-connected ordinal Element of W

L . u1 is non empty Element of W

u2 is set

i is Element of l

u . i is set

a is epsilon-transitive epsilon-connected ordinal Element of W

L . a is non empty Element of W

(L . u1) /\ (bool lambda) is set

l /\ (bool lambda) is set

(bool lambda) /\ (bool lambda) is set

(Union L) /\ ((bool lambda) /\ (bool lambda)) is Element of bool W

lambda is set

dom L is epsilon-transitive epsilon-connected ordinal set

l is set

L . l is set

u is epsilon-transitive epsilon-connected ordinal set

On W is non empty epsilon-transitive epsilon-connected ordinal set

u1 is epsilon-transitive epsilon-connected ordinal Element of W

L . u1 is non empty Element of W

u2 is set

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

variables_in W is non empty Element of bool VAR

Free W is V35() Element of bool VAR

W <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 3),(Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

L is non empty set

[:VAR,L:] is set

bool [:VAR,L:] is set

ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

def_func' (W,ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]

[:L,L:] is set

bool [:L,L:] is set

lambda is Element of VAR

W / ((x. 0),lambda) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free (W / ((x. 0),lambda)) is V35() Element of bool VAR

(W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 0),(All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 3),(Ex ((x. 0),(All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

def_func' ((W / ((x. 0),lambda)),ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]

l is Element of L

ksi / ((x. 3),l) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

u is Element of L

u2 is Element of L

(ksi / ((x. 3),l)) / ((x. 4),u2) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

u1 is Element of L

((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda is Element of L

((ksi / ((x. 3),l)) / ((x. 4),u2)) / ((x. 0),(((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda is Element of L

((ksi / ((x. 3),l)) / ((x. 4),u2)) / ((x. 0),(((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

l is set

u is Element of L

(def_func' (W,ksi)) . u is Element of L

ksi / ((x. 3),u) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) . lambda is Element of L

((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) / ((x. 0),(((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(def_func' (W,ksi)) . l is set

(def_func' ((W / ((x. 0),lambda)),ksi)) . l is set

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

W <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 3),(Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free W is V35() Element of bool VAR

L is non empty set

[:VAR,L:] is set

bool [:VAR,L:] is set

ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

def_func' (W,ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]

[:L,L:] is set

bool [:L,L:] is set

the Element of L is Element of L

ksi / ((x. 3), the Element of L) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

l is Element of L

(ksi / ((x. 3), the Element of L)) / ((x. 0),l) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

u is Element of L

(def_func' (W,ksi)) .: u is Element of bool L

bool L is set

the Element of (def_func' (W,ksi)) .: u is Element of (def_func' (W,ksi)) .: u

dom (def_func' (W,ksi)) is Element of bool L

u2 is set

(def_func' (W,ksi)) . u2 is set

i is Element of L

((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i)) . (x. 4) is Element of L

(((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i)) . (x. 0) is Element of L

((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) . (x. 0) is Element of L

a is Element of L

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

variables_in W is non empty Element of bool VAR

Free W is V35() Element of bool VAR

L is Element of VAR

W / ((x. 0),L) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

(W / ((x. 0),L)) / ((x. 4),(x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

ksi is Element of VAR

(x. 3) 'in' ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free (Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR

Free (((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() Element of bool VAR

{(x. 3)} is non empty trivial V35() 1 -element set

(Free (((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool VAR

Free ((x. 3) 'in' ksi) is V35() Element of bool VAR

Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))) is V35() Element of bool VAR

(Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() Element of bool VAR

((Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool VAR

{(x. 3),ksi} is V35() set

{(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() set

({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool ({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))))

bool ({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) is V35() V39() set

{(x. 3),ksi} \ {(x. 3)} is V35() Element of bool {(x. 3),ksi}

bool {(x. 3),ksi} is V35() V39() set

(Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) \ {(x. 3)} is V35() Element of bool VAR

({(x. 3),ksi} \ {(x. 3)}) \/ ((Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) \ {(x. 3)}) is V35() set

Free (W / ((x. 0),L)) is V35() Element of bool VAR

{(x. 0)} is non empty trivial V35() 1 -element set

(Free W) \ {(x. 0)} is V35() Element of bool VAR

{L} is non empty trivial V35() 1 -element set

((Free W) \ {(x. 0)}) \/ {L} is V35() set

{(x. 0)} is non empty trivial V35() 1 -element set

variables_in (W / ((x. 0),L)) is non empty Element of bool VAR

{(x. 4)} is non empty trivial V35() 1 -element set

(Free (W / ((x. 0),L))) \ {(x. 4)} is V35() Element of bool VAR

((Free (W / ((x. 0),L))) \ {(x. 4)}) \/ {(x. 0)} is V35() set

(Free W) \ {(x. 0)} is V35() Element of bool VAR

{L} is non empty trivial V35() 1 -element set

((Free W) \ {(x. 0)}) \/ {L} is V35() set

W is non empty epsilon-transitive V33() V34() universal set

L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set

Union L is non empty Element of bool W

bool W is set

[:VAR,(Union L):] is set

bool [:VAR,(Union L):] is set

lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free lambda is V35() Element of bool VAR

l is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

lambda <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 0),(All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 3),(Ex ((x. 0),(All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

variables_in lambda is non empty Element of bool VAR

u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

u + 5 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

x. (u + 5) is Element of VAR

lambda / ((x. 0),(x. (u + 5))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

u + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

(lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 0),(All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

All ((x. 3),(Ex ((x. 0),(All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

def_func' (lambda,l) is Relation-like Union L -defined Union L -valued Function-like quasi_total Element of bool [:(Union L),(Union L):]

[:(Union L),(Union L):] is set

bool [:(Union L),(Union L):] is set

def_func' ((lambda / ((x. 0),(x. (u + 5)))),l) is Relation-like Union L -defined Union L -valued Function-like quasi_total Element of bool [:(Union L),(Union L):]

i is Element of Union L

dom L is epsilon-transitive epsilon-connected ordinal set

a is set

L . a is set

On W is non empty epsilon-transitive epsilon-connected ordinal set

i is epsilon-transitive epsilon-connected ordinal Element of W

L . i is set

i is Relation-like Function-like set

dom i is set

rng i is set

a is set

i is set

i . i is set

i is Element of Union L

i . i is set

b is epsilon-transitive epsilon-connected ordinal Element of W

L . b is non empty Element of W

card VAR is non empty epsilon-transitive epsilon-connected ordinal cardinal set

card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set

dom l is Element of bool VAR

card (dom l) is epsilon-transitive epsilon-connected ordinal cardinal set

rng l is Element of bool (Union L)

bool (Union L) is set

l .: (dom l) is Element of bool (Union L)

card (rng l) is epsilon-transitive epsilon-connected ordinal cardinal set

i .: (rng l) is set

card (i .: (rng l)) is epsilon-transitive epsilon-connected ordinal cardinal set

sup (i .: (rng l)) is epsilon-transitive epsilon-connected ordinal set

Free (lambda / ((x. 0),(x. (u + 5)))) is V35() Element of bool VAR

i is set

i .: i is set

sup (i .: i) is epsilon-transitive epsilon-connected ordinal set

i is epsilon-transitive epsilon-connected ordinal Element of W

L . i is non empty Element of W

b is set

e is Element of Union L

i . e is set

e is epsilon-transitive epsilon-connected ordinal Element of W

L . e is non empty Element of W

i is Element of Union L

i . i is set

i is epsilon-transitive epsilon-connected ordinal Element of W

L . i is non empty Element of W

card i is epsilon-transitive epsilon-connected ordinal cardinal set

variables_in (lambda / ((x. 0),(x. (u + 5)))) is non empty Element of bool VAR

(def_func' (lambda,l)) .: i is Element of bool (Union L)

i .: ((def_func' (lambda,l)) .: i) is set

card (i .: ((def_func' (lambda,l)) .: i)) is epsilon-transitive epsilon-connected ordinal cardinal set

card ((def_func' (lambda,l)) .: i) is epsilon-transitive epsilon-connected ordinal cardinal set

sup (i .: ((def_func' (lambda,l)) .: i)) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal Element of W

i \/ b is epsilon-transitive epsilon-connected ordinal Element of W

a is epsilon-transitive epsilon-connected ordinal Element of W

(i \/ b) \/ a is epsilon-transitive epsilon-connected ordinal Element of W

L . (i \/ b) is non empty Element of W

On W is non empty epsilon-transitive epsilon-connected ordinal set

[:(On W),(On W):] is set

bool [:(On W),(On W):] is set

(lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

phi is Relation-like On W -defined On W -valued Function-like T-Sequence-like quasi_total Ordinal-yielding Element of bool [:(On W),(On W):]

a1 is epsilon-transitive epsilon-connected ordinal Element of W

phi . a1 is epsilon-transitive epsilon-connected ordinal Element of W

L . a1 is non empty Element of W

x is set

q is set

l . q is set

mu is Element of VAR

l . mu is Element of Union L

i . (l . mu) is set

v is epsilon-transitive epsilon-connected ordinal Element of W

L . v is non empty Element of W

10 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT

u + 10 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

x. (u + 10) is Element of VAR

{(x. 0)} is non empty trivial V35() 1 -element set

(variables_in lambda) \ {(x. 0)} is Element of bool VAR

(x. 3) 'in' (x. (u + 10)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

10 + u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

[:VAR,(L . a1):] is set

bool [:VAR,(L . a1):] is set

v is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

v . (x. 4) is Element of L . a1

v / ((x. 0),(v . (x. 4))) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

mu is Element of L . a1

(v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

{(x. (u + 5))} is non empty trivial V35() 1 -element set

((variables_in lambda) \ {(x. 0)}) \/ {(x. (u + 5))} is set

variables_in ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))) is non empty Element of bool VAR

{(x. 4)} is non empty trivial V35() 1 -element set

(variables_in (lambda / ((x. 0),(x. (u + 5))))) \ {(x. 4)} is Element of bool VAR

((variables_in (lambda / ((x. 0),(x. (u + 5))))) \ {(x. 4)}) \/ {(x. 0)} is set

((Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))),(L . a1),((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu))) is Element of bool (L . a1)

bool (L . a1) is set

Free (Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR

u1 is set

dom (def_func' (lambda,l)) is Element of bool (Union L)

m1 is set

(def_func' (lambda,l)) . m1 is set

u9 is Element of Union L

l / ((x. 3),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

(def_func' (lambda,l)) . u9 is Element of Union L

(l / ((x. 3),u9)) / ((x. 0),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

u2 is Element of L . a1

v / ((x. 3),u2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

m2 is Element of L . a1

(v / ((x. 3),u2)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

(Union L) ! ((v / ((x. 3),u2)) / ((x. 0),m2)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

(l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9))) . (x. 4) is Element of Union L

((l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9))) / ((x. 0),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((l / ((x. 3),u9)) / ((x. 0),((def_func' (lambda,l)) . u9))) / ((x. 4),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((v / ((x. 3),u2)) / ((x. 0),m2)) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1

((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) . (x. (u + 10)) is Element of L . a1

(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2)) . (x. 3) is Element of L . a1

((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2)) . (x. (u + 10)) is Element of L . a1

v / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

(v / ((x. (u + 10)),mu)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

{ b

u1 is set

{ b

m1 is Element of L . a1

((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

m2 is Element of L . a1

(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

v / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

(v / ((x. (u + 10)),mu)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

v / ((x. 3),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

(v / ((x. 3),m2)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]

u2 is Element of Union L

l / ((x. 3),u2) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

u9 is Element of Union L

(l / ((x. 3),u2)) / ((x. 0),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((l / ((x. 3),u2)) / ((x. 0),u9)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

(l / ((x. 3),u2)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((l / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

((l / ((x. 3),u2)) / ((x. 0),u9)) . (x. 0) is Element of Union L

(Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]

(def_func' (lambda,l)) . u2 is Element of Union L

((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1

(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) . (x. (u + 10)) is Element of L . a1

dom (def_func' (lambda,l)) is Element of bool (Union L)

((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) is Element of L . a1

((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (u + 10)) is Element of L . a1

Free (Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR

lambda is set

dom L is epsilon-transitive epsilon-connected ordinal set

l is set

L . l is set

u is epsilon-transitive epsilon-connected ordinal set

u1 is epsilon-transitive epsilon-connected ordinal Element of W

L . u1 is non empty Element of W

u2 is set

lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free lambda is V35() Element of bool VAR

the_axiom_of_substitution_for lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free W is V35() Element of bool VAR

code (Free W) is V35() Element of bool NAT

L is non empty set

[:VAR,L:] is set

bool [:VAR,L:] is set

ksi is Element of L

lambda is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

lambda * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

[:NAT,L:] is non trivial V35() set

bool [:NAT,L:] is non trivial V35() set

l is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

x. l is Element of VAR

[l,ksi] is set

{l,ksi} is V35() set

{l} is non empty trivial V35() V39() 1 -element set

{{l,ksi},{l}} is V35() V39() set

{[l,ksi]} is Function-like non empty trivial V35() 1 -element set

(code (Free W)) \ {l} is V35() Element of bool NAT

(lambda * decode) | ((code (Free W)) \ {l}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

{[l,ksi]} \/ ((lambda * decode) | ((code (Free W)) \ {l})) is V35() set

lambda / ((x. l),ksi) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(lambda / ((x. l),ksi)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

((lambda / ((x. l),ksi)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

((lambda / ((x. l),ksi)) * decode) | {l} is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

dom (((lambda / ((x. l),ksi)) * decode) | {l}) is V35() Element of bool NAT

dom ((lambda / ((x. l),ksi)) * decode) is Element of bool NAT

(dom ((lambda / ((x. l),ksi)) * decode)) /\ {l} is V35() Element of bool NAT

NAT /\ {l} is V35() set

(((lambda / ((x. l),ksi)) * decode) | {l}) . l is set

[l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)] is set

{l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)} is V35() set

{{l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)},{l}} is V35() V39() set

{[l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)]} is Function-like non empty trivial V35() 1 -element set

((lambda / ((x. l),ksi)) * decode) . l is set

[l,(((lambda / ((x. l),ksi)) * decode) . l)] is set

{l,(((lambda / ((x. l),ksi)) * decode) . l)} is V35() set

{{l,(((lambda / ((x. l),ksi)) * decode) . l)},{l}} is V35() V39() set

{[l,(((lambda / ((x. l),ksi)) * decode) . l)]} is Function-like non empty trivial V35() 1 -element set

x". (x. l) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

((lambda / ((x. l),ksi)) * decode) . (x". (x. l)) is set

[l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))] is set

{l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))} is V35() set

{{l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))},{l}} is V35() V39() set

{[l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))]} is Function-like non empty trivial V35() 1 -element set

(lambda / ((x. l),ksi)) . (x. l) is Element of L

[l,((lambda / ((x. l),ksi)) . (x. l))] is set

{l,((lambda / ((x. l),ksi)) . (x. l))} is V35() set

{{l,((lambda / ((x. l),ksi)) . (x. l))},{l}} is V35() V39() set

{[l,((lambda / ((x. l),ksi)) . (x. l))]} is Function-like non empty trivial V35() 1 -element set

dom ((lambda * decode) | ((code (Free W)) \ {l})) is V35() Element of bool NAT

dom (lambda * decode) is Element of bool NAT

(dom (lambda * decode)) /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT

NAT /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT

(dom ((lambda / ((x. l),ksi)) * decode)) /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT

((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

dom (((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l})) is V35() Element of bool NAT

i is set

a is Element of VAR

x". a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

((lambda * decode) | ((code (Free W)) \ {l})) . i is set

(lambda * decode) . i is set

lambda . a is Element of L

(lambda / ((x. l),ksi)) . a is Element of L

((lambda / ((x. l),ksi)) * decode) . i is set

(((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l})) . i is set

{l} \/ ((code (Free W)) \ {l}) is V35() set

((lambda / ((x. l),ksi)) * decode) | ({l} \/ ((code (Free W)) \ {l})) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

{{}} is non empty trivial V35() 1 -element set

W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free W is V35() Element of bool VAR

code (Free W) is V35() Element of bool NAT

(code (Free W)) \ {{}} is V35() Element of bool NAT

L is non empty set

[:VAR,L:] is set

bool [:VAR,L:] is set

Diagram (W,L) is set

ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(W,L,ksi) is Element of bool L

bool L is set

ksi * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

[:NAT,L:] is non trivial V35() set

bool [:NAT,L:] is non trivial V35() set

(ksi * decode) | ((code (Free W)) \ {{}}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

{ b

{ b

u is set

u1 is Element of L

[{},u1] is set

{{},u1} is V35() set

{{{},u1},{{}}} is V35() V39() set

{[{},u1]} is Function-like non empty trivial V35() 1 -element set

{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set

ksi / ((x. 0),u1) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

(ksi / ((x. 0),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

((ksi / ((x. 0),u1)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

St (W,L) is Element of bool (VAL L)

VAL L is set

bool (VAL L) is set

u2 is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

u2 * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

(u2 * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

u is set

u1 is Element of L

ksi / ((x. 0),u1) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

St (W,L) is Element of bool (VAL L)

VAL L is set

bool (VAL L) is set

(ksi / ((x. 0),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

((ksi / ((x. 0),u1)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

[{},u1] is set

{{},u1} is V35() set

{{{},u1},{{}}} is V35() V39() set

{[{},u1]} is Function-like non empty trivial V35() 1 -element set

{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set

the Element of { b

u1 is Element of L

[{},u1] is set

{{},u1} is V35() set

{{{},u1},{{}}} is V35() V39() set

{[{},u1]} is Function-like non empty trivial V35() 1 -element set

{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set

St (W,L) is Element of bool (VAL L)

VAL L is set

bool (VAL L) is set

u2 is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]

u2 * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]

(u2 * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

i is Relation-like Function-like set

dom i is set

dom (u2 * decode) is Element of bool NAT

(dom (u2 * decode)) /\ (code (Free W)) is V35() Element of bool NAT

a is Element of VAR

x". a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

W is non empty epsilon-transitive V33() V34() universal set

bool W is set

L is non empty Element of bool W

ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

lambda is non empty set

[:VAR,lambda:] is set

bool [:VAR,lambda:] is set

l is Relation-like VAR -defined lambda -valued Function-like quasi_total Element of bool [:VAR,lambda:]

(ksi,lambda,l) is Element of bool lambda

bool lambda is set

Free ksi is V35() Element of bool VAR

Free ksi is V35() Element of bool VAR

code (Free ksi) is V35() Element of bool NAT

u1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

{u1} is non empty trivial V35() V39() 1 -element set

(code (Free ksi)) \ {u1} is V35() Element of bool NAT

Diagram (ksi,lambda) is set

i is Element of W

((code (Free ksi)) \ {u1}) \/ {u1} is V35() set

u is Element of W

Funcs ((((code (Free ksi)) \ {u1}) \/ {u1}),u) is set

a is set

St (ksi,lambda) is Element of bool (VAL lambda)

VAL lambda is set

bool (VAL lambda) is set

Funcs ((code (Free ksi)),u) is set

i is Relation-like VAR -defined lambda -valued Function-like quasi_total Element of bool [:VAR,lambda:]

i * decode is Relation-like NAT -defined lambda -valued Function-like Element of bool [:NAT,lambda:]

[:NAT,lambda:] is non trivial V35() set

bool [:NAT,lambda:] is non trivial V35() set

(i * decode) | (code (Free ksi)) is Relation-like NAT -defined lambda -valued Function-like V35() Element of bool [:NAT,lambda:]

x". (x. 0) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

l * decode is Relation-like NAT -defined lambda -valued Function-like Element of bool [:NAT,lambda:]

[:NAT,lambda:] is non trivial V35() set

bool [:NAT,lambda:] is non trivial V35() set

(l * decode) | ((code (Free ksi)) \ {u1}) is Relation-like NAT -defined lambda -valued Function-like V35() Element of bool [:NAT,lambda:]

Funcs (((code (Free ksi)) \ {u1}),u) is set

a is Element of W

{ b

{ b

b is set

e is Element of W

[u1,e] is set

{u1,e} is V35() set

{{u1,e},{u1}} is V35() V39() set

{[u1,e]} is Function-like non empty trivial V35() 1 -element set

{[u1,e]} \/ a is set

b is set

e is Element of lambda

[u1,e] is set

{u1,e} is V35() set

{{u1,e},{u1}} is V35() V39() set

{[u1,e]} is Function-like non empty trivial V35() 1 -element set

{[u1,e]} \/ a is set

e is Element of W

Free ksi is V35() Element of bool VAR

W is non empty epsilon-transitive V33() V34() universal set

L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set

Union L is non empty Element of bool W

bool W is set

ksi is set

dom L is epsilon-transitive epsilon-connected ordinal set

lambda is set

L . lambda is set

l is epsilon-transitive epsilon-connected ordinal set

On W is non empty epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal Element of W

L . u is non empty Element of W

u1 is set

ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

Free ksi is V35() Element of bool VAR

the_axiom_of_substitution_for ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

ksi is set

union ksi is set

ksi is set

lambda is set

{ksi,lambda} is V35() set

card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set

{ b

inf { b

0-element_of W is epsilon-transitive epsilon-connected ordinal Element of W

ksi is Relation-like Function-like set

dom ksi is set

ksi . 0 is set

rng ksi is set

card (rng ksi) is epsilon-transitive epsilon-connected ordinal cardinal set

card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal set

sup (rng ksi) is epsilon-transitive epsilon-connected ordinal set

On W is non empty epsilon-transitive epsilon-connected ordinal set

l is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . l is set

l + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . (l + 1) is set

u is epsilon-transitive epsilon-connected ordinal Element of W

L . u is non empty Element of W

{ b

inf { b

dom L is epsilon-transitive epsilon-connected ordinal set

u1 is set

L . u1 is set

u2 is epsilon-transitive epsilon-connected ordinal Element of W

l is set

u is set

ksi . u is set

u1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . u1 is set

u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . u is set

L . (ksi . u) is set

u + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . (u + 1) is set

L . (ksi . (u + 1)) is set

dom L is epsilon-transitive epsilon-connected ordinal set

u1 is epsilon-transitive epsilon-connected ordinal Element of W

L . u1 is non empty Element of W

u2 is set

L . u2 is set

i is epsilon-transitive epsilon-connected ordinal Element of W

{ b

{ b

inf { b

a is Element of W

L . a is set

u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . u is set

u + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . (u + 1) is set

u1 is epsilon-transitive epsilon-connected ordinal Element of W

u2 is epsilon-transitive epsilon-connected ordinal Element of W

L . u1 is non empty Element of W

L . u2 is non empty Element of W

l is epsilon-transitive epsilon-connected ordinal Element of W

union l is epsilon-transitive epsilon-connected ordinal Element of W

u is epsilon-transitive epsilon-connected ordinal set

u1 is epsilon-transitive epsilon-connected ordinal set

u2 is set

ksi . u2 is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

i + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . (i + 1) is set

a is epsilon-transitive epsilon-connected ordinal Element of W

{ (L . (ksi . b

union { (L . (ksi . b

L . l is non empty Element of W

u1 is set

u2 is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . i is set

L . (ksi . i) is set

a is epsilon-transitive epsilon-connected ordinal Element of W

L . a is non empty Element of W

L | l is Relation-like rng L -valued Function-like T-Sequence-like set

rng L is V68() set

Union (L | l) is set

u1 is set

dom (L | l) is epsilon-transitive epsilon-connected ordinal set

u2 is set

(L | l) . u2 is set

L . u2 is set

dom L is epsilon-transitive epsilon-connected ordinal set

(dom L) /\ l is set

i is epsilon-transitive epsilon-connected ordinal Element of W

a is epsilon-transitive epsilon-connected ordinal set

i is set

ksi . i is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . i is set

b is epsilon-transitive epsilon-connected ordinal Element of W

L . i is non empty Element of W

L . b is non empty Element of W

L . (ksi . i) is set

L . (sup (rng ksi)) is set

u is set

u1 is set

u2 is set

i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . i is set

L . (ksi . i) is set

a is epsilon-transitive epsilon-connected ordinal Element of W

L . a is non empty Element of W

i + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT

ksi . (i + 1) is set

L . (ksi . (i + 1)) is set

ksi is set