:: ZF_MODEL semantic presentation

K96() is set

K100() is Element of K27(K96())

K27(K96()) is non empty set

omega is set

K27(omega) is non empty set

K27(K100()) is non empty set

VAR is non empty Element of K27(K100())

1 is non empty Element of K100()

0 is empty Element of K100()

2 is non empty Element of K100()

3 is non empty Element of K100()

4 is non empty Element of K100()

{} is empty set

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 E is Element of VAR

Var2 E is Element of VAR

F

F

x is set

[E,x] is set

{E,x} is non empty set

{E} is non empty set

{{E,x},{E}} is non empty set

{ [(b

{ [(b

{ [(b

E is set

E . 1 is set

(Var1 E) 'in' (Var2 E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var1 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130((Var1 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130((Var1 E))),K130((Var2 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

f is Element of VAR

f is Element of VAR

f '=' f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(f) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(f) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(f)),K130(f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(f '=' f),F

{(f '=' f),F

{(f '=' f)} is non empty set

{{(f '=' f),F

f 'in' f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K117(K100(),K121(K100(),1),K130(f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(f)),K130(f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(f 'in' f),F

{(f 'in' f),F

{(f 'in' f)} is non empty set

{{(f 'in' f),F

(Var1 E) '=' (Var2 E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130((Var1 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130((Var1 E))),K130((Var2 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 f is Element of VAR

Var2 f is Element of VAR

F

F

the_argument_of f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

bound_in f is Element of VAR

the_scope_of f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[f,f] is set

{f,f} is non empty set

{f} is non empty set

{{f,f},{f}} is non empty set

g is Element of VAR

h is Element of VAR

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

f . 1 is set

(Var1 f) '=' (Var2 f) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130((Var1 f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130((Var1 f))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130((Var1 f))),K130((Var2 f))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

g is Element of VAR

h is Element of VAR

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

g is Element of VAR

h is Element of VAR

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

(Var1 f) 'in' (Var2 f) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130((Var1 f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130((Var1 f))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 f)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130((Var1 f))),K130((Var2 f))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

g is Element of VAR

h is Element of VAR

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

E . 1 is set

E is set

x is set

[(the_left_argument_of E),x] is set

{(the_left_argument_of E),x} is non empty set

{(the_left_argument_of E)} is non empty set

{{(the_left_argument_of E),x},{(the_left_argument_of E)}} is non empty set

f is set

f is set

[(the_right_argument_of E),f] is set

{(the_right_argument_of E),f} is non empty set

{(the_right_argument_of E)} is non empty set

{{(the_right_argument_of E),f},{(the_right_argument_of E)}} is non empty set

F

g is set

[E,g] is set

{E,g} is non empty set

{E} is non empty set

{{E,g},{E}} is non empty set

E \/ f is set

{[E,g]} is non empty set

(E \/ f) \/ {[E,g]} is non empty set

h is non empty set

z is Element of VAR

b2 is Element of VAR

z '=' b2 is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(z) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(z)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(b2) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(z)),K130(b2)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(z '=' b2),F

{(z '=' b2),F

{(z '=' b2)} is non empty set

{{(z '=' b2),F

z 'in' b2 is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(z)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(z)),K130(b2)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(z 'in' b2),F

{(z 'in' b2),F

{(z 'in' b2)} is non empty set

{{(z 'in' b2),F

z is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 z is Element of VAR

Var2 z is Element of VAR

F

F

the_argument_of z is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of z is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of z is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

bound_in z is Element of VAR

the_scope_of z is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

b2 is set

[z,b2] is set

{z,b2} is non empty set

{z} is non empty set

{{z,b2},{z}} is non empty set

c

F

[(the_argument_of z),c

{(the_argument_of z),c

{(the_argument_of z)} is non empty set

{{(the_argument_of z),c

c

F

[(the_argument_of z),c

{(the_argument_of z),c

{{(the_argument_of z),c

c

F

[(the_argument_of z),c

{(the_argument_of z),c

{{(the_argument_of z),c

d is set

F

[(the_argument_of z),d] is set

{(the_argument_of z),d} is non empty set

{{(the_argument_of z),d},{(the_argument_of z)}} is non empty set

c

d is set

F

[(the_left_argument_of z),c

{(the_left_argument_of z),c

{(the_left_argument_of z)} is non empty set

{{(the_left_argument_of z),c

[(the_right_argument_of z),d] is set

{(the_right_argument_of z),d} is non empty set

{(the_right_argument_of z)} is non empty set

{{(the_right_argument_of z),d},{(the_right_argument_of z)}} is non empty set

c

d is set

F

[(the_left_argument_of z),c

{(the_left_argument_of z),c

{{(the_left_argument_of z),c

[(the_right_argument_of z),d] is set

{(the_right_argument_of z),d} is non empty set

{{(the_right_argument_of z),d},{(the_right_argument_of z)}} is non empty set

[(the_right_argument_of z),f] is set

{(the_right_argument_of z),f} is non empty set

{{(the_right_argument_of z),f},{(the_right_argument_of z)}} is non empty set

[(the_left_argument_of z),x] is set

{(the_left_argument_of z),x} is non empty set

{{(the_left_argument_of z),x},{(the_left_argument_of z)}} is non empty set

c

d is set

F

[(the_left_argument_of z),c

{(the_left_argument_of z),c

{{(the_left_argument_of z),c

[(the_right_argument_of z),d] is set

{(the_right_argument_of z),d} is non empty set

{{(the_right_argument_of z),d},{(the_right_argument_of z)}} is non empty set

c

c

F

[(the_left_argument_of z),c

{(the_left_argument_of z),c

{{(the_left_argument_of z),c

[(the_right_argument_of z),c

{(the_right_argument_of z),c

{{(the_right_argument_of z),c

c

c

F

[(the_left_argument_of z),c

{(the_left_argument_of z),c

{{(the_left_argument_of z),c

[(the_right_argument_of z),c

{(the_right_argument_of z),c

{{(the_right_argument_of z),c

c

F

[(the_scope_of z),c

{(the_scope_of z),c

{(the_scope_of z)} is non empty set

{{(the_scope_of z),c

c

F

[(the_scope_of z),c

{(the_scope_of z),c

{{(the_scope_of z),c

c

F

[(the_scope_of z),c

{(the_scope_of z),c

{{(the_scope_of z),c

d is set

F

[(the_scope_of z),d] is set

{(the_scope_of z),d} is non empty set

{{(the_scope_of z),d},{(the_scope_of z)}} is non empty set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

E . 1 is set

E is set

x is set

[(the_scope_of E),x] is set

{(the_scope_of E),x} is non empty set

{(the_scope_of E)} is non empty set

{{(the_scope_of E),x},{(the_scope_of E)}} is non empty set

bound_in E is Element of VAR

F

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

{[E,f]} is non empty set

E \/ {[E,f]} is non empty set

f is non empty set

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 g is Element of VAR

Var2 g is Element of VAR

F

F

the_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

bound_in g is Element of VAR

the_scope_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

h is set

[g,h] is set

{g,h} is non empty set

{g} is non empty set

{{g,h},{g}} is non empty set

z is set

F

[(the_argument_of g),z] is set

{(the_argument_of g),z} is non empty set

{(the_argument_of g)} is non empty set

{{(the_argument_of g),z},{(the_argument_of g)}} is non empty set

z is set

b2 is set

F

[(the_left_argument_of g),z] is set

{(the_left_argument_of g),z} is non empty set

{(the_left_argument_of g)} is non empty set

{{(the_left_argument_of g),z},{(the_left_argument_of g)}} is non empty set

[(the_right_argument_of g),b2] is set

{(the_right_argument_of g),b2} is non empty set

{(the_right_argument_of g)} is non empty set

{{(the_right_argument_of g),b2},{(the_right_argument_of g)}} is non empty set

z is set

F

[(the_scope_of g),z] is set

{(the_scope_of g),z} is non empty set

{(the_scope_of g)} is non empty set

{{(the_scope_of g),z},{(the_scope_of g)}} is non empty set

[(the_scope_of g),x] is set

{(the_scope_of g),x} is non empty set

{{(the_scope_of g),x},{(the_scope_of g)}} is non empty set

z is set

F

[(the_scope_of g),z] is set

{(the_scope_of g),z} is non empty set

{{(the_scope_of g),z},{(the_scope_of g)}} is non empty set

b2 is set

F

[(the_scope_of g),b2] is set

{(the_scope_of g),b2} is non empty set

{{(the_scope_of g),b2},{(the_scope_of g)}} is non empty set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

E . 1 is set

E is set

x is set

[(the_argument_of E),x] is set

{(the_argument_of E),x} is non empty set

{(the_argument_of E)} is non empty set

{{(the_argument_of E),x},{(the_argument_of E)}} is non empty set

F

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

{[E,f]} is non empty set

E \/ {[E,f]} is non empty set

f is non empty set

g is Element of VAR

h is Element of VAR

g '=' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(g) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(h) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g '=' h),F

{(g '=' h),F

{(g '=' h)} is non empty set

{{(g '=' h),F

g 'in' h is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(g)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(g)),K130(h)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

F

[(g 'in' h),F

{(g 'in' h),F

{(g 'in' h)} is non empty set

{{(g 'in' h),F

g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 g is Element of VAR

Var2 g is Element of VAR

F

F

the_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

bound_in g is Element of VAR

the_scope_of g is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

h is set

[g,h] is set

{g,h} is non empty set

{g} is non empty set

{{g,h},{g}} is non empty set

z is set

F

[(the_argument_of g),z] is set

{(the_argument_of g),z} is non empty set

{(the_argument_of g)} is non empty set

{{(the_argument_of g),z},{(the_argument_of g)}} is non empty set

[(the_argument_of g),x] is set

{(the_argument_of g),x} is non empty set

{{(the_argument_of g),x},{(the_argument_of g)}} is non empty set

z is set

F

[(the_argument_of g),z] is set

{(the_argument_of g),z} is non empty set

{{(the_argument_of g),z},{(the_argument_of g)}} is non empty set

b2 is set

F

[(the_argument_of g),b2] is set

{(the_argument_of g),b2} is non empty set

{{(the_argument_of g),b2},{(the_argument_of g)}} is non empty set

z is set

b2 is set

F

[(the_left_argument_of g),z] is set

{(the_left_argument_of g),z} is non empty set

{(the_left_argument_of g)} is non empty set

{{(the_left_argument_of g),z},{(the_left_argument_of g)}} is non empty set

[(the_right_argument_of g),b2] is set

{(the_right_argument_of g),b2} is non empty set

{(the_right_argument_of g)} is non empty set

{{(the_right_argument_of g),b2},{(the_right_argument_of g)}} is non empty set

z is set

F

[(the_scope_of g),z] is set

{(the_scope_of g),z} is non empty set

{(the_scope_of g)} is non empty set

{{(the_scope_of g),z},{(the_scope_of g)}} is non empty set

F

F

[F

{F

{F

{{F

F

[F

{F

{{F

E is set

E is set

x is set

x is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

f is set

[E,f] is set

{E,f} is non empty set

{{E,f},{E}} is non empty set

bound_in E is Element of VAR

g is set

F

[(the_scope_of E),g] is set

{(the_scope_of E),g} is non empty set

{(the_scope_of E)} is non empty set

{{(the_scope_of E),g},{(the_scope_of E)}} is non empty set

h is set

F

[(the_scope_of E),h] is set

{(the_scope_of E),h} is non empty set

{{(the_scope_of E),h},{(the_scope_of E)}} is non empty set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

f is set

[E,f] is set

{E,f} is non empty set

{{E,f},{E}} is non empty set

Var1 E is Element of VAR

Var2 E is Element of VAR

F

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

f is set

[E,f] is set

{E,f} is non empty set

{{E,f},{E}} is non empty set

g is set

h is set

F

[(the_left_argument_of E),g] is set

{(the_left_argument_of E),g} is non empty set

{(the_left_argument_of E)} is non empty set

{{(the_left_argument_of E),g},{(the_left_argument_of E)}} is non empty set

[(the_right_argument_of E),h] is set

{(the_right_argument_of E),h} is non empty set

{(the_right_argument_of E)} is non empty set

{{(the_right_argument_of E),h},{(the_right_argument_of E)}} is non empty set

z is set

b2 is set

F

[(the_left_argument_of E),z] is set

{(the_left_argument_of E),z} is non empty set

{{(the_left_argument_of E),z},{(the_left_argument_of E)}} is non empty set

[(the_right_argument_of E),b2] is set

{(the_right_argument_of E),b2} is non empty set

{{(the_right_argument_of E),b2},{(the_right_argument_of E)}} is non empty set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

f is set

[E,f] is set

{E,f} is non empty set

{{E,f},{E}} is non empty set

g is set

F

[(the_argument_of E),g] is set

{(the_argument_of E),g} is non empty set

{(the_argument_of E)} is non empty set

{{(the_argument_of E),g},{(the_argument_of E)}} is non empty set

h is set

F

[(the_argument_of E),h] is set

{(the_argument_of E),h} is non empty set

{{(the_argument_of E),h},{(the_argument_of E)}} is non empty set

F

F

Var1 F

Var2 F

F

F

the_argument_of F

F

F

the_left_argument_of F

F

the_right_argument_of F

F

bound_in F

the_scope_of F

F

F

[F

{F

{F

{{F

E is set

x is set

F

[(the_argument_of F

{(the_argument_of F

{(the_argument_of F

{{(the_argument_of F

x is set

E is set

F

[(the_left_argument_of F

{(the_left_argument_of F

{(the_left_argument_of F

{{(the_left_argument_of F

[(the_right_argument_of F

{(the_right_argument_of F

{(the_right_argument_of F

{{(the_right_argument_of F

f is set

f is set

F

x is set

F

[(the_scope_of F

{(the_scope_of F

{(the_scope_of F

{{(the_scope_of F

F

F

x is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

[E,x] is set

{E,x} is non empty set

{E} is non empty set

{{E,x},{E}} is non empty set

f is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

Var1 E is Element of VAR

Var2 E is Element of VAR

F

F

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

F

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

bound_in E is Element of VAR

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

F

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

F

bound_in E is Element of VAR

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

F

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

F

Var1 E is Element of VAR

Var2 E is Element of VAR

F

F

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

x is set

[E,x] is set

{E,x} is non empty set

{E} is non empty set

{{E,x},{E}} is non empty set

E is set

[E,E] is set

{E,E} is non empty set

{{E,E},{E}} is non empty set

x is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E) is set

[E,x] is set

{E,x} is non empty set

{E} is non empty set

{{E,x},{E}} is non empty set

f is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

f is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

(E) is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E) is set

Var1 E is Element of VAR

Var2 E is Element of VAR

{(Var1 E),(Var2 E)} is non empty set

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_argument_of E)) is set

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_left_argument_of E)) is set

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_right_argument_of E)) is set

bound_in E is Element of VAR

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_scope_of E)) is set

{H

union {H

{(bound_in E)} is non empty set

(union {H

K27((union {H

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E) is set

K27(VAR) is non empty set

x is Element of VAR

E is Element of VAR

{x,E} is non empty set

f is set

x is set

E is set

{x,E} is non empty set

union {x,E} is set

f is set

f is set

x is set

{x} is non empty set

union {x} is set

E is Element of VAR

{E} is non empty set

(union {x}) \ {E} is Element of K27((union {x}))

K27((union {x})) is non empty set

f is set

f is set

x is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E) is Element of K27(VAR)

Var1 E is Element of VAR

Var2 E is Element of VAR

{(Var1 E),(Var2 E)} is non empty set

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_argument_of E)) is Element of K27(VAR)

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_left_argument_of E)) is Element of K27(VAR)

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_right_argument_of E)) is Element of K27(VAR)

((the_left_argument_of E)) \/ ((the_right_argument_of E)) is Element of K27(VAR)

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_scope_of E)) is Element of K27(VAR)

bound_in E is Element of VAR

{(bound_in E)} is non empty set

((the_scope_of E)) \ {(bound_in E)} is Element of K27(VAR)

{((the_left_argument_of E)),((the_right_argument_of E))} is non empty set

union {((the_left_argument_of E)),((the_right_argument_of E))} is set

{((the_scope_of E))} is non empty set

union {((the_scope_of E))} is set

(union {((the_scope_of E))}) \ {(bound_in E)} is Element of K27((union {((the_scope_of E))}))

K27((union {((the_scope_of E))})) is non empty set

E is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

E is non empty set

(E) is set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

x is non empty set

(x) is non empty set

Funcs (VAR,x) is non empty FUNCTION_DOMAIN of VAR ,x

K28(VAR,x) is non empty set

K27(K28(VAR,x)) is non empty set

{ b

( not b

{ b

( not b

K27((x)) is non empty set

{ b

for b

( not b

( ex b

( not b

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

E is set

[E,E] is set

{E,E} is non empty set

{E} is non empty set

{{E,E},{E}} is non empty set

f is set

[E,f] is set

{E,f} is non empty set

{{E,f},{E}} is non empty set

x is non empty set

(x) is non empty set

Funcs (VAR,x) is non empty FUNCTION_DOMAIN of VAR ,x

K28(VAR,x) is non empty set

K27(K28(VAR,x)) is non empty set

{ b

( not b

{ b

( not b

K27((x)) is non empty set

{ b

for b

( not b

( ex b

( not b

f is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E,x) is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

h is set

f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

g is set

[f,g] is set

{f,g} is non empty set

{f} is non empty set

{{f,g},{f}} is non empty set

(f,x) is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E,x) is set

Var1 E is Element of VAR

Var2 E is Element of VAR

{ b

( not b

{ b

( not b

the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_argument_of E),x) is set

{H

union {H

(x) \ (union {H

the_left_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_left_argument_of E),x) is set

the_right_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_right_argument_of E),x) is set

bound_in E is Element of VAR

the_scope_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_scope_of E),x) is set

{ b

for b

( not b

( ex b

( not b

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

x is non empty set

(E,x) is set

(x) is non empty set

Funcs (VAR,x) is non empty FUNCTION_DOMAIN of VAR ,x

K27((x)) is non empty set

K28(VAR,x) is non empty set

K27(K28(VAR,x)) is non empty set

{ b

for b

( not b

( ex b

( not b

{ b

( not b

{ b

( not b

E is set

{E} is non empty set

union {E} is set

(x) \ (union {E}) is Element of K27((x))

E is set

f is set

{E} is non empty set

union {E} is set

{f} is non empty set

union {f} is set

(union {E}) /\ (union {f}) is set

f is Element of K27((x))

{f} is non empty set

union {f} is set

(union {f}) /\ (union {f}) is set

g is set

E is Element of VAR

f is Element of VAR

{ b

( not b

{ b

( not b

h is set

z is Element of (x)

h is set

z is Element of (x)

E is Element of VAR

f is Element of VAR

{ b

( not b

f is Element of VAR

g is Element of VAR

{ b

( not b

E is set

f is Element of VAR

{ b

for b

( not b

( ex b

( not b

g is set

h is Element of (x)

f is set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E,x) is set

[E,f] is set

{E,f} is non empty set

{E} is non empty set

{{E,f},{E}} is non empty set

h is set

f is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

g is set

[f,g] is set

{f,g} is non empty set

{f} is non empty set

{{f,g},{f}} is non empty set

(f,x) is set

E is non empty set

K28(VAR,E) is non empty set

K27(K28(VAR,E)) is non empty set

x is Element of VAR

E is Element of VAR

x '=' E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(x) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130(x)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(E) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130(x)),K130(E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

((x '=' E),E) is Element of K27((E))

(E) is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

K27((E)) is non empty set

f is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

f . x is Element of E

f . E is Element of E

Var1 (x '=' E) is Element of VAR

Var2 (x '=' E) is Element of VAR

(Var1 (x '=' E)) '=' (Var2 (x '=' E)) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130((Var1 (x '=' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130((Var1 (x '=' E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 (x '=' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130((Var1 (x '=' E)))),K130((Var2 (x '=' E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

{ b

( not b

f is Element of (E)

g is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

g . (Var1 (x '=' E)) is Element of E

g . (Var2 (x '=' E)) is Element of E

f is Element of (E)

E is non empty set

K28(VAR,E) is non empty set

K27(K28(VAR,E)) is non empty set

x is Element of VAR

E is Element of VAR

x 'in' E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(x) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130(x)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(E) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130(x)),K130(E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

((x 'in' E),E) is Element of K27((E))

(E) is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

K27((E)) is non empty set

f is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

f . x is Element of E

f . E is Element of E

Var1 (x 'in' E) is Element of VAR

Var2 (x 'in' E) is Element of VAR

(Var1 (x 'in' E)) 'in' (Var2 (x 'in' E)) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130((Var1 (x 'in' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130((Var1 (x 'in' E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 (x 'in' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130((Var1 (x 'in' E)))),K130((Var2 (x 'in' E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

{ b

( not b

f is Element of (E)

g is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

g . (Var1 (x 'in' E)) is Element of E

g . (Var2 (x 'in' E)) is Element of E

f is Element of (E)

E is non empty set

K28(VAR,E) is non empty set

K27(K28(VAR,E)) is non empty set

x is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(x,E) is Element of K27((E))

(E) is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

K27((E)) is non empty set

'not' x is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),2) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),2),x) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

(('not' x),E) is Element of K27((E))

E is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

{(x,E)} is non empty set

union {(x,E)} is set

the_argument_of ('not' x) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E) \ (x,E) is Element of K27((E))

E is non empty set

K28(VAR,E) is non empty set

K27(K28(VAR,E)) is non empty set

x is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(x,E) is Element of K27((E))

(E) is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

K27((E)) is non empty set

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E,E) is Element of K27((E))

x '&' E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),3) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),3),x) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),3),x),E) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

((x '&' E),E) is Element of K27((E))

f is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

{(x,E)} is non empty set

union {(x,E)} is set

{(E,E)} is non empty set

union {(E,E)} is set

the_left_argument_of (x '&' E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_left_argument_of (x '&' E)),E) is Element of K27((E))

{((the_left_argument_of (x '&' E)),E)} is non empty set

union {((the_left_argument_of (x '&' E)),E)} is set

the_right_argument_of (x '&' E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_right_argument_of (x '&' E)),E) is Element of K27((E))

{((the_right_argument_of (x '&' E)),E)} is non empty set

union {((the_right_argument_of (x '&' E)),E)} is set

(union {((the_left_argument_of (x '&' E)),E)}) /\ (union {((the_right_argument_of (x '&' E)),E)}) is set

(the_left_argument_of (x '&' E)) '&' (the_right_argument_of (x '&' E)) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K117(K100(),K121(K100(),3),(the_left_argument_of (x '&' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),3),(the_left_argument_of (x '&' E))),(the_right_argument_of (x '&' E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

E is non empty set

K28(VAR,E) is non empty set

K27(K28(VAR,E)) is non empty set

x is Element of VAR

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

(E,E) is Element of K27((E))

(E) is non empty set

Funcs (VAR,E) is non empty FUNCTION_DOMAIN of VAR ,E

K27((E)) is non empty set

All (x,E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),4) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130(x) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),4),K130(x)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),4),K130(x)),E) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

((All (x,E)),E) is Element of K27((E))

f is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

the_scope_of (All (x,E)) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

((the_scope_of (All (x,E))),E) is Element of K27((E))

bound_in (All (x,E)) is Element of VAR

{ b

for b

( not b

( ex b

( not b

All ((bound_in (All (x,E))),(the_scope_of (All (x,E)))) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K130((bound_in (All (x,E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),4),K130((bound_in (All (x,E))))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),4),K130((bound_in (All (x,E))))),(the_scope_of (All (x,E)))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

f is Element of (E)

g is set

h is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

z is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

f is Element of (E)

f is V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E))

g is Element of (E)

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 E is Element of VAR

Var2 E is Element of VAR

x is non empty set

K28(VAR,x) is non empty set

K27(K28(VAR,x)) is non empty set

(E,x) is Element of K27((x))

(x) is non empty set

Funcs (VAR,x) is non empty FUNCTION_DOMAIN of VAR ,x

K27((x)) is non empty set

(Var1 E) '=' (Var2 E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),0) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var1 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),0),K130((Var1 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),0),K130((Var1 E))),K130((Var2 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

E is V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x))

E . (Var1 E) is Element of x

E . (Var2 E) is Element of x

f is V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x))

f . (Var1 E) is Element of x

f . (Var2 E) is Element of x

E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

Var1 E is Element of VAR

Var2 E is Element of VAR

x is non empty set

K28(VAR,x) is non empty set

K27(K28(VAR,x)) is non empty set

(E,x) is Element of K27((x))

(x) is non empty set

Funcs (VAR,x) is non empty FUNCTION_DOMAIN of VAR ,x

K27((x)) is non empty set

(Var1 E) 'in' (Var2 E) is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())

K121(K100(),1) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var1 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K121(K100(),1),K130((Var1 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K130((Var2 E)) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

K117(K100(),K117(K100(),K121(K100(),1),K130((Var1 E))),K130((Var2 E))) is V1() V4(K100()) V5(K100()) Function-like V36() M7(K100())

E is V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x))

E . (Var1 E) is Element of x

E . (Var2 E) is