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:86;
A2: x. 3 <> x. 4 by ZF_LANG1:86;
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:86;

now

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:80;
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:82;
set f1 = ((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m;

now

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:130;
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:34, ZF_LANG1:86;
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:34, ZF_LANG1:86;
A16: ((((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4 by FUNCT_7:130;
A17: (((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m by FUNCT_7:130;
A18: ((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m by FUNCT_7:130;
A19: M,((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 )) by A12, ZF_LANG1:80;

A20: now

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, Th6;
then M,(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H by A7, A8, A9, A11, A1, A2, Th8;
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, Th10;
hence M,(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H / y,x by A5, Th13; :: thesis: verum

end;

now

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, Th13;
then M,(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H by A6, Th10;
then M,(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,(v . y) |= H by A7, A8, A9, A11, A1, A2, Th8;
then M,((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H by A5, Th6;
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:80;
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:82; :: 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:80; :: thesis: def_func' H,v = def_func' (H / y,x),(v / x,(v . y))
A22: Free H c= variables_in H by ZF_LANG1:164;
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 9 :: 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, Th11;
then M,((v / (x. 3),a) / (x. 4),((def_func' H,v) . a)) / x,(v . y) |= H by A5, Th6;
then M,((v / x,(v . y)) / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H by A8, A9, A2, Th7;
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, Th14;
then M,((v / x,(v . y)) / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H / y,x by A23, Th10;
hence (def_func' H,v) . a = (def_func' (H / y,x),(v / x,(v . y))) . a by A10, A21, Th11; :: thesis: verum