let F1, F2 be Function of E,E; :: thesis: ( ( for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F2 . (g . (x. 3)) = g . (x. 4) ) ) implies F1 = F2 )
assume that
A55: for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) and
A56: for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F2 . (g . (x. 3)) = g . (x. 4) ) ; :: thesis: F1 = F2
let a be Element of E; :: according to FUNCT_2:def 9 :: thesis: F1 . a = F2 . a
set f = val +* (x. 3),a;
for x being Variable st (val +* (x. 3),a) . x <> val . x holds
x. 3 = x by FUNCT_7:34;
then E,val +* (x. 3),a |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A2, ZF_MODEL:16;
then consider g being Function of VAR ,E such that
A57: for x being Variable st g . x <> (val +* (x. 3),a) . x holds
x. 0 = x and
A58: E,g |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_MODEL:20;
A59: g . (x. 3) = (val +* (x. 3),a) . (x. 3) by A57;
set h = g +* (x. 4),(g . (x. 0 ));

A60: now

let x be Variable; :: thesis: ( (g +* (x. 4),(g . (x. 0 ))) . x <> val . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A61: ( (g +* (x. 4),(g . (x. 0 ))) . x <> val . x & x. 0 <> x ) and
A62: ( x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction
( (val +* (x. 3),a) . x = val . x & (g +* (x. 4),(g . (x. 0 ))) . x = g . x ) by A62, FUNCT_7:34;
hence contradiction by A57, A61; :: thesis: verum

end;

( (g +* (x. 4),(g . (x. 0 ))) . (x. 4) = g . (x. 0 ) & (g +* (x. 4),(g . (x. 0 ))) . (x. 0 ) = g . (x. 0 ) ) by FUNCT_7:34, FUNCT_7:130;
then A63: E,g +* (x. 4),(g . (x. 0 )) |= (x. 4) '=' (x. 0 ) by ZF_MODEL:12;
A64: ( (val +* (x. 3),a) . (x. 3) = a & (g +* (x. 4),(g . (x. 0 ))) . (x. 3) = g . (x. 3) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (g +* (x. 4),(g . (x. 0 ))) . x <> g . x holds
x. 4 = x by FUNCT_7:34;
then E,g +* (x. 4),(g . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A58, ZF_MODEL:16;
then A65: E,g +* (x. 4),(g . (x. 0 )) |= H by A63, ZF_MODEL:19;
then F1 . ((g +* (x. 4),(g . (x. 0 ))) . (x. 3)) = (g +* (x. 4),(g . (x. 0 ))) . (x. 4) by A55, A60;
hence F1 . a = F2 . a by A56, A65, A60, A64, A59; :: thesis: verum