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
F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
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
F1((Var1 E),(Var2 E)) is set
F2((Var1 E),(Var2 E)) is set
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
{ [(b1 '=' b2),F1(b1,b2)] where b1, b2 is Element of VAR : b1 = b1 } is set
{ [(b1 'in' b2),F2(b1,b2)] where b1, b2 is Element of VAR : b1 = b1 } is set
{ [(b1 '=' b2),F1(b1,b2)] where b1, b2 is Element of VAR : b1 = b1 } \/ { [(b1 'in' b2),F2(b1,b2)] where b1, b2 is Element of VAR : b1 = b1 } is set
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())
F1(f,f) is set
[(f '=' f),F1(f,f)] is set
{(f '=' f),F1(f,f)} is non empty set
{(f '=' f)} is non empty set
{{(f '=' f),F1(f,f)},{(f '=' f)}} is non empty set
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())
F2(f,f) is set
[(f 'in' f),F2(f,f)] is set
{(f 'in' f),F2(f,f)} is non empty set
{(f 'in' f)} is non empty set
{{(f 'in' f),F2(f,f)},{(f 'in' f)}} 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())
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
F1((Var1 f),(Var2 f)) is set
F2((Var1 f),(Var2 f)) is set
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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} is non empty set
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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} 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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} 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())
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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} is non empty set
(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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} 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())
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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} 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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} 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())
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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} is non empty set
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
F4(x,f) is set
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())
F1(z,b2) is set
[(z '=' b2),F1(z,b2)] is set
{(z '=' b2),F1(z,b2)} is non empty set
{(z '=' b2)} is non empty set
{{(z '=' b2),F1(z,b2)},{(z '=' b2)}} is non empty set
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())
F2(z,b2) is set
[(z 'in' b2),F2(z,b2)] is set
{(z 'in' b2),F2(z,b2)} is non empty set
{(z 'in' b2)} is non empty set
{{(z 'in' b2),F2(z,b2)},{(z 'in' b2)}} is non empty set
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
F1((Var1 z),(Var2 z)) is set
F2((Var1 z),(Var2 z)) is set
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
c10 is set
F3(c10) is set
[(the_argument_of z),c10] is set
{(the_argument_of z),c10} is non empty set
{(the_argument_of z)} is non empty set
{{(the_argument_of z),c10},{(the_argument_of z)}} is non empty set
c10 is set
F3(c10) is set
[(the_argument_of z),c10] is set
{(the_argument_of z),c10} is non empty set
{{(the_argument_of z),c10},{(the_argument_of z)}} is non empty set
c10 is set
F3(c10) is set
[(the_argument_of z),c10] is set
{(the_argument_of z),c10} is non empty set
{{(the_argument_of z),c10},{(the_argument_of z)}} is non empty set
d is set
F3(d) is set
[(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
c10 is set
d is set
F4(c10,d) is set
[(the_left_argument_of z),c10] is set
{(the_left_argument_of z),c10} is non empty set
{(the_left_argument_of z)} is non empty set
{{(the_left_argument_of z),c10},{(the_left_argument_of z)}} is non empty set
[(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
c10 is set
d is set
F4(c10,d) is set
[(the_left_argument_of z),c10] is set
{(the_left_argument_of z),c10} is non empty set
{{(the_left_argument_of z),c10},{(the_left_argument_of z)}} is non empty set
[(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
c10 is set
d is set
F4(c10,d) is set
[(the_left_argument_of z),c10] is set
{(the_left_argument_of z),c10} is non empty set
{{(the_left_argument_of z),c10},{(the_left_argument_of z)}} is non empty set
[(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
c12 is set
c13 is set
F4(c12,c13) is set
[(the_left_argument_of z),c12] is set
{(the_left_argument_of z),c12} is non empty set
{{(the_left_argument_of z),c12},{(the_left_argument_of z)}} is non empty set
[(the_right_argument_of z),c13] is set
{(the_right_argument_of z),c13} is non empty set
{{(the_right_argument_of z),c13},{(the_right_argument_of z)}} is non empty set
c14 is set
c15 is set
F4(c14,c15) is set
[(the_left_argument_of z),c14] is set
{(the_left_argument_of z),c14} is non empty set
{{(the_left_argument_of z),c14},{(the_left_argument_of z)}} is non empty set
[(the_right_argument_of z),c15] is set
{(the_right_argument_of z),c15} is non empty set
{{(the_right_argument_of z),c15},{(the_right_argument_of z)}} is non empty set
c10 is set
F5((bound_in z),c10) is set
[(the_scope_of z),c10] is set
{(the_scope_of z),c10} is non empty set
{(the_scope_of z)} is non empty set
{{(the_scope_of z),c10},{(the_scope_of z)}} is non empty set
c10 is set
F5((bound_in z),c10) is set
[(the_scope_of z),c10] is set
{(the_scope_of z),c10} is non empty set
{{(the_scope_of z),c10},{(the_scope_of z)}} is non empty set
c10 is set
F5((bound_in z),c10) is set
[(the_scope_of z),c10] is set
{(the_scope_of z),c10} is non empty set
{{(the_scope_of z),c10},{(the_scope_of z)}} is non empty set
d is set
F5((bound_in z),d) is set
[(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
F5((bound_in E),x) is set
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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} is non empty set
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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} is non empty set
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
F1((Var1 g),(Var2 g)) is set
F2((Var1 g),(Var2 g)) is set
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
F3(z) is set
[(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
F4(z,b2) is set
[(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
F5((bound_in g),z) is set
[(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
F5((bound_in g),z) is set
[(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
F5((bound_in g),b2) is set
[(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
F3(x) is set
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())
F1(g,h) is set
[(g '=' h),F1(g,h)] is set
{(g '=' h),F1(g,h)} is non empty set
{(g '=' h)} is non empty set
{{(g '=' h),F1(g,h)},{(g '=' h)}} is non empty set
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())
F2(g,h) is set
[(g 'in' h),F2(g,h)] is set
{(g 'in' h),F2(g,h)} is non empty set
{(g 'in' h)} is non empty set
{{(g 'in' h),F2(g,h)},{(g 'in' h)}} is non empty set
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
F1((Var1 g),(Var2 g)) is set
F2((Var1 g),(Var2 g)) is set
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
F3(z) is set
[(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
F3(z) is set
[(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
F3(b2) is set
[(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
F4(z,b2) is set
[(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
F5((bound_in g),z) is set
[(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
F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7() is set
[F6(),F7()] is set
{F6(),F7()} is non empty set
{F6()} is non empty set
{{F6(),F7()},{F6()}} is non empty set
F8() is set
[F6(),F8()] is set
{F6(),F8()} is non empty set
{{F6(),F8()},{F6()}} is non empty set
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
F5((bound_in E),g) is set
[(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
F5((bound_in E),h) is set
[(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
F2((Var1 E),(Var2 E)) is set
F1((Var1 E),(Var2 E)) is set
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
F4(g,h) is set
[(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
F4(z,b2) is set
[(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
F3(g) is set
[(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
F3(h) is set
[(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
F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7(F6()) is set
Var1 F6() is Element of VAR
Var2 F6() is Element of VAR
F1((Var1 F6()),(Var2 F6())) is set
F2((Var1 F6()),(Var2 F6())) is set
the_argument_of F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7((the_argument_of F6())) is set
F3(F7((the_argument_of F6()))) is set
the_left_argument_of F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7((the_left_argument_of F6())) is set
the_right_argument_of F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7((the_right_argument_of F6())) is set
bound_in F6() is Element of VAR
the_scope_of F6() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F7((the_scope_of F6())) is set
F5((bound_in F6()),F7((the_scope_of F6()))) is set
[F6(),F7(F6())] is set
{F6(),F7(F6())} is non empty set
{F6()} is non empty set
{{F6(),F7(F6())},{F6()}} is non empty set
E is set
x is set
F3(x) is set
[(the_argument_of F6()),x] is set
{(the_argument_of F6()),x} is non empty set
{(the_argument_of F6())} is non empty set
{{(the_argument_of F6()),x},{(the_argument_of F6())}} is non empty set
x is set
E is set
F4(x,E) is set
[(the_left_argument_of F6()),x] is set
{(the_left_argument_of F6()),x} is non empty set
{(the_left_argument_of F6())} is non empty set
{{(the_left_argument_of F6()),x},{(the_left_argument_of F6())}} is non empty set
[(the_right_argument_of F6()),E] is set
{(the_right_argument_of F6()),E} is non empty set
{(the_right_argument_of F6())} is non empty set
{{(the_right_argument_of F6()),E},{(the_right_argument_of F6())}} is non empty set
f is set
f is set
F4(f,f) is set
x is set
F5((bound_in F6()),x) is set
[(the_scope_of F6()),x] is set
{(the_scope_of F6()),x} is non empty set
{(the_scope_of F6())} is non empty set
{{(the_scope_of F6()),x},{(the_scope_of F6())}} is non empty set
F7() is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F6(F7()) is set
x is set
E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F6(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
F6(E) is set
E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F6(E) is set
Var1 E is Element of VAR
Var2 E is Element of VAR
F1((Var1 E),(Var2 E)) is set
F2((Var1 E),(Var2 E)) is set
the_argument_of E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F6((the_argument_of E)) is set
F3(H1( 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())
F6((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())
F6((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())
F6((the_scope_of E)) is set
F5((bound_in E),H1( the_scope_of E)) is 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())
F6((the_argument_of E)) is set
F6(E) is set
F3(F6((the_argument_of E))) 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())
F6((the_scope_of E)) is set
F6(E) is set
bound_in E is Element of VAR
F5((bound_in E),F6((the_scope_of E))) is set
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())
F6((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())
F6((the_right_argument_of E)) is set
F6(E) is set
F4(F6((the_left_argument_of E)),F6((the_right_argument_of E))) is set
E is V1() V4(K100()) V5(K100()) Function-like V36() ZF-formula-like M7(K100())
F6(E) is set
Var1 E is Element of VAR
Var2 E is Element of VAR
F1((Var1 E),(Var2 E)) is set
F2((Var1 E),(Var2 E)) is set
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
{H6( the_scope_of E)} is non empty set
union {H6( the_scope_of E)} is set
{(bound_in E)} is non empty set
(union {H6( the_scope_of E)}) \ {(bound_in E)} is Element of K27((union {H6( the_scope_of E)}))
K27((union {H6( the_scope_of E)})) is non empty set
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
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 = b2 . a2 ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 in b2 . a2 ) } is set
K27((x)) is non empty set
{ b1 where b1 is Element of (x) : for b2 being set
for b3 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = a2 or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not a1 = b5 ) or b4 in b2 ) ) ) ) } is set
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
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 = b2 . a2 ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 in b2 . a2 ) } is set
K27((x)) is non empty set
{ b1 where b1 is Element of (x) : for b2 being set
for b3 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = a2 or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not a1 = b5 ) or b4 in b2 ) ) ) ) } is set
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
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . (Var1 E) = b2 . (Var2 E) ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . (Var1 E) in b2 . (Var2 E) ) } is set
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
{H12( the_argument_of E)} is non empty set
union {H12( the_argument_of E)} is set
(x) \ (union {H12( the_argument_of E)}) is Element of K27((x))
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
{ b1 where b1 is Element of (x) : for b2 being set
for b3 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = H12( the_scope_of E) or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not bound_in E = b5 ) or b4 in b2 ) ) ) ) } is set
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
{ b1 where b1 is Element of (x) : for b2 being set
for b3 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = a2 or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not a1 = b5 ) or b4 in b2 ) ) ) ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 in b2 . a2 ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . a1 = b2 . a2 ) } is set
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
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . E = b2 . f ) } is set
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . E in b2 . f ) } is set
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
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . E = b2 . f ) } is set
f is Element of VAR
g is Element of VAR
{ b1 where b1 is Element of (x) : for b2 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = b1 or b2 . f in b2 . g ) } is set
E is set
f is Element of VAR
{ b1 where b1 is Element of (x) : for b2 being set
for b3 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( not b2 = E or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(x) Function-like quasi_total Element of K27(K28(VAR,x)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not f = b5 ) or b4 in b2 ) ) ) ) } is set
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())
{ b1 where b1 is Element of (E) : for b2 being V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E)) holds
( not b2 = b1 or b2 . (Var1 (x '=' E)) = b2 . (Var2 (x '=' E)) ) } is set
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())
{ b1 where b1 is Element of (E) : for b2 being V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E)) holds
( not b2 = b1 or b2 . (Var1 (x 'in' E)) in b2 . (Var2 (x 'in' E)) ) } is set
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
{ b1 where b1 is Element of (E) : for b2 being set
for b3 being V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E)) holds
( not b2 = ((the_scope_of (All (x,E))),E) or not b3 = b1 or ( b3 in b2 & ( for b4 being V1() V4( VAR ) V5(E) Function-like quasi_total Element of K27(K28(VAR,E)) holds
( ex b5 being Element of VAR st
( not b4 . b5 = b3 . b5 & not bound_in (All (x,E)) = b5 ) or b4 in b2 ) ) ) ) } is set
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