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
A33: 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
A34: 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;
A35: ( (val +* (x. 3),a) . (x. 3) = a & ( for x being Variable st x <> x. 3 holds
(val +* (x. 3),a) . x = val . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (val +* (x. 3),a) . x <> val . x holds
x. 3 = x by A35;
then E,val +* (x. 3),a |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A1, ZF_MODEL:16;
then consider g being Function of VAR ,E such that
A36: ( ( for x being Variable st g . x <> (val +* (x. 3),a) . x holds
x. 0 = x ) & E,g |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) ) by ZF_MODEL:20;
set h = g +* (x. 4),(g . (x. 0 ));
A37: ( (g +* (x. 4),(g . (x. 0 ))) . (x. 4) = g . (x. 0 ) & ( for x being Variable st x <> x. 4 holds
(g +* (x. 4),(g . (x. 0 ))) . x = g . x ) ) 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 A37;
then A38: E,g +* (x. 4),(g . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A36, ZF_MODEL:16;
(g +* (x. 4),(g . (x. 0 ))) . (x. 0 ) = g . (x. 0 ) by A37;
then E,g +* (x. 4),(g . (x. 0 )) |= (x. 4) '=' (x. 0 ) by A37, ZF_MODEL:12;
then A39: E,g +* (x. 4),(g . (x. 0 )) |= H by A38, ZF_MODEL:19;

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
A40: (g +* (x. 4),(g . (x. 0 ))) . x <> val . x and
A41: ( x. 0 <> x & x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction
( (val +* (x. 3),a) . x = val . x & g . x = (val +* (x. 3),a) . x & (g +* (x. 4),(g . (x. 0 ))) . x = g . x ) by A35, A36, A37, A41;
hence contradiction by A40; :: thesis: verum

end;

then A42: ( F1 . ((g +* (x. 4),(g . (x. 0 ))) . (x. 3)) = (g +* (x. 4),(g . (x. 0 ))) . (x. 4) & F2 . ((g +* (x. 4),(g . (x. 0 ))) . (x. 3)) = (g +* (x. 4),(g . (x. 0 ))) . (x. 4) ) by A33, A34, A39;
( (g +* (x. 4),(g . (x. 0 ))) . (x. 3) = g . (x. 3) & g . (x. 3) = (val +* (x. 3),a) . (x. 3) ) by A36, A37;
hence F1 . a = F2 . a by A35, A42; :: thesis: verum