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 8 :: 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:32;
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 :: thesis: for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x & x. 3 <> x holds
not x. 4 <> x

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:32;
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:32, FUNCT_7:128;
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:32, FUNCT_7:128;
for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> g . x holds
x. 4 = x by FUNCT_7:32;
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