let x, y be Variable; :: thesis: for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let M be non empty set ; :: thesis: for H being ZF-formula
for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let H be ZF-formula; :: thesis: for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let v be Function of VAR,M; :: thesis: ( not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 implies ( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) ) )
A1: x. 0 <> x. 4 by ZF_LANG1:76;
A2: x. 3 <> x. 4 by ZF_LANG1:76;
set F = H / (y,x);
set f = v / (x,(v . y));
assume that
A3: not x. 0 in Free H and
A4: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and
A5: not x in variables_in H and
A6: not y in Free H and
A7: x <> x. 0 and
A8: x <> x. 3 and
A9: x <> x. 4 ; :: thesis: ( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
( ( Free (H / (y,x)) c= variables_in (H / (y,x)) & not x. 0 in variables_in (H / (y,x)) ) or ( not x. 0 in {x} & not x. 0 in (Free H) \ {y} ) ) by A3, A7, TARSKI:def 1, XBOOLE_0:def 5;
then ( not x. 0 in Free (H / (y,x)) or ( Free (H / (y,x)) c= ((Free H) \ {y}) \/ {x} & not x. 0 in ((Free H) \ {y}) \/ {x} ) ) by Th1, XBOOLE_0:def 3;
hence A10: not x. 0 in Free (H / (y,x)) ; :: thesis: ( M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
A11: x. 0 <> x. 3 by ZF_LANG1:76;

now :: thesis: for m3 being Element of M holds M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))

let m3 be Element of M; :: thesis: M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))
M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A4, ZF_LANG1:71;
then consider m being Element of M such that
A12: M,(v / ((x. 3),m3)) / ((x. 0),m) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
set f1 = ((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m);

now :: thesis: for m4 being Element of M holds M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0))

let m4 be Element of M; :: thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0))
A13: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
A14: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A15: ((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = (((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A16: ((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
A17: (((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A18: ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A19: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A12, ZF_LANG1:71;

A20: now :: thesis: ( M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) implies M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) )

assume M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ; :: thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x)
then m = m4 by A16, A15, A17, ZF_MODEL:12;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A13, A14, A18, ZF_MODEL:12;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A19, ZF_MODEL:19;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,(v . y)) |= H by A5, Th5;
then M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A7, A8, A9, A11, A1, A2, Th7;
then M,((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (y,(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x)) |= H by A6, Th9;
hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) by A5, Th12; :: thesis: verum

end;

now :: thesis: ( M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) implies M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) )

assume M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) ; :: thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)
then M,((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (y,(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x)) |= H by A5, Th12;
then M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A6, Th9;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,(v . y)) |= H by A7, A8, A9, A11, A1, A2, Th7;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A5, Th5;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A19, ZF_MODEL:19;
then m = m4 by A13, A14, A18, ZF_MODEL:12;
hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A16, A15, A17, ZF_MODEL:12; :: thesis: verum

end;

hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0)) by A20, ZF_MODEL:19; :: thesis: verum

end;

then M,((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m) |= All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; :: thesis: verum

end;

hence A21: M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; :: thesis: def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y))))
A22: Free H c= variables_in H by ZF_LANG1:151;
Free (H / (y,x)) = Free H by A5, A6, Th2;
then A23: not x in Free (H / (y,x)) by A5, A22;
let a be Element of M; :: according to FUNCT_2:def 8 :: thesis: (def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a
set a9 = (def_func' (H,v)) . a;
M,(v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H by A3, A4, Th10;
then M,((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,(v . y)) |= H by A5, Th5;
then M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H by A8, A9, A2, Th6;
then M,(((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,((((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . y)) |= H / (y,x) by A5, Th13;
then M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H / (y,x) by A23, Th9;
hence (def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a by A10, A21, Th10; :: thesis: verum