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) )
let g be Function of VAR ,E; :: thesis: ( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
set j = f +* (x. 3),(g . (x. 3));
set h = (f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4));

A3: 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
A4: ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x and
x. 0 <> x and
A5: x. 3 <> x and
A6: 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, FUNCT_7:34
.= f . x by A5, FUNCT_7:34 ;
hence contradiction by A4; :: thesis: verum

end;

A7: ( not x. 0 in Free H & E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ) by A1, A2, TARSKI:def 2, ZF_MODEL:def 5;
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

set g3 = f +* (x. 3),(g . (x. 3));
set g4 = (f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4));

A8: 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
A9: ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> f . x and
x. 0 <> x and
A10: x. 3 <> x and
A11: 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 A11, FUNCT_7:34
.= f . x by A10, FUNCT_7:34 ;
hence contradiction by A9; :: thesis: verum

end;

A12: (f +* (x. 3),(g . (x. 3))) . (x. 3) = g . (x. 3) by FUNCT_7:130;

A13: 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 g . x <> ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x ; :: thesis: not x in Free H
then ( x. 4 <> x & x. 3 <> x ) by A12, FUNCT_7:34, FUNCT_7:130;
hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

end;

assume E,g |= H ; :: thesis: F . (g . (x. 3)) = g . (x. 4)
then E,(f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4)) |= H by A13, Th14;
then ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) = g . (x. 4) & 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 A7, A8, Def1, FUNCT_7:130;
hence F . (g . (x. 3)) = g . (x. 4) by A12, FUNCT_7:34; :: thesis: verum

end;

assume that
A14: F . (g . (x. 3)) = g . (x. 4) and
A15: not E,g |= H ; :: thesis: contradiction
A16: (f +* (x. 3),(g . (x. 3))) . (x. 3) = g . (x. 3) by 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 ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . x <> g . x ; :: thesis: not x in Free H
then ( x. 4 <> x & x. 3 <> x ) by A16, FUNCT_7:34, FUNCT_7:130;
hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

end;

then not E,(f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4)) |= H by A15, Th14;
then ( ((f +* (x. 3),(g . (x. 3))) +* (x. 4),(g . (x. 4))) . (x. 4) = g . (x. 4) & 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 A7, A3, Def1, FUNCT_7:130;
hence contradiction by A14, A16, FUNCT_7:34; :: thesis: verum