set f = the Function of VAR,E;
take F = def_func' (H, the Function of VAR,E); :: 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 = the Function of VAR,E +* ((x. 3),(g . (x. 3)));
set h = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

A3: now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x holds
not x. 4 <> x

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A4: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and
x. 0 <> x and
A5: x. 3 <> x and
A6: x. 4 <> x ; :: thesis: contradiction
(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A6, FUNCT_7:32
.= the Function of VAR,E . x by A5, FUNCT_7:32 ;
hence contradiction by A4; :: thesis: verum

end;

A7: ( not x. 0 in Free H & E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) by A1, A2, TARSKI:def 2;
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 = the Function of VAR,E +* ((x. 3),(g . (x. 3)));
set g4 = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));

A8: now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x holds
not x. 4 <> x

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A9: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and
x. 0 <> x and
A10: x. 3 <> x and
A11: x. 4 <> x ; :: thesis: contradiction
(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A11, FUNCT_7:32
.= the Function of VAR,E . x by A10, FUNCT_7:32 ;
hence contradiction by A9; :: thesis: verum

end;

A12: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;

A13: now :: thesis: for x being Variable st g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x holds
not x in Free H

let x be Variable; :: thesis: ( g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x implies not x in Free H )
assume g . x <> (( the Function of VAR,E +* ((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:32, FUNCT_7:128;
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,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A13, Th13;
then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) = (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A8, Def1, FUNCT_7:128;
hence F . (g . (x. 3)) = g . (x. 4) by A12, FUNCT_7:32; :: thesis: verum

end;

assume that
A14: F . (g . (x. 3)) = g . (x. 4) and
A15: not E,g |= H ; :: thesis: contradiction
A16: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;

now :: thesis: for x being Variable st (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x holds
not x in Free H

let x be Variable; :: thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x implies not x in Free H )
assume (( the Function of VAR,E +* ((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:32, FUNCT_7:128;
hence not x in Free H by A1, TARSKI:def 2; :: thesis: verum

end;

then not E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A15, Th13;
then ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A3, Def1, FUNCT_7:128;
hence contradiction by A14, A16, FUNCT_7:32; :: thesis: verum