consider f being Function of VAR ,E;
take F = def_func' H,f; :: thesis: for g being Function of VAR ,E holds
( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
A2: not x. 0 in Free H by A1, TARSKI:def 2;
A3: E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by A1, ZF_MODEL:def 5;
let g be Function of VAR ,E; :: thesis: ( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
thus ( E,g |= H implies F . (g . (x. 3)) = g . (x. 4) ) :: thesis: ( F . (g . (x. 3)) = g . (x. 4) implies E,g |= H )

proof

assume A4: E,g |= H ; :: thesis: F . (g . (x. 3)) = g . (x. 4)
set g3 = f +* (x. 3),(g . (x. 3));
A5: ( (f +* (x. 3),(g . (x. 3))) . (x. 3) = g . (x. 3) & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),(g . (x. 3))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set g4 = (f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4));
A6: ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) = g . (x. 4) & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x = (f +* (x. 3),(g . (x. 3))) . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let x be Variable; :: thesis: ( g . x <> ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x implies not x in Free H )
assume A7: g . x <> ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x ; :: thesis: not x in Free H
then A8: x. 4 <> x by A6;
x. 3 <> x by A5, A6, A7;
hence not x in Free H by A1, A8, TARSKI:def 2; :: thesis: verum

end;

then A9: E,(f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4)) |= H by A4, Th14;

now

let x be Variable; :: thesis: ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A10: ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x and
A11: ( x. 0 <> x & x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction
((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x = (f +* (x. 3),(g . (x. 3))) . x by A6, A11
.= f . x by A5, A11 ;
hence contradiction by A10; :: thesis: verum

end;

then F . (((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 3)) = ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) by A2, A3, A9, Def1;
hence F . (g . (x. 3)) = g . (x. 4) by A5, A6; :: thesis: verum

end;

assume that
A12: F . (g . (x. 3)) = g . (x. 4) and
A13: not E,g |= H ; :: thesis: contradiction
set j = f +* (x. 3),(g . (x. 3));
A14: ( (f +* (x. 3),(g . (x. 3))) . (x. 3) = g . (x. 3) & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),(g . (x. 3))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set h = (f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4));
A15: ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) = g . (x. 4) & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x = (f +* (x. 3),(g . (x. 3))) . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let x be Variable; :: thesis: ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> g . x implies not x in Free H )
assume A16: ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> g . x ; :: thesis: not x in Free H
then A17: x. 4 <> x by A15;
x. 3 <> x by A14, A15, A16;
hence not x in Free H by A1, A17, TARSKI:def 2; :: thesis: verum

end;

then A18: not E,(f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4)) |= H by A13, Th14;

now

let x be Variable; :: thesis: ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A19: ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x and
A20: ( x. 0 <> x & x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction
((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x = (f +* (x. 3),(g . (x. 3))) . x by A15, A20
.= f . x by A14, A20 ;
hence contradiction by A19; :: thesis: verum

end;

then F . (((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 3)) <> ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) by A2, A3, A18, Def1;
hence contradiction by A12, A14, A15; :: thesis: verum