consider f being Function of VAR ,E;
let F1, F2 be Function of E,E; :: thesis: ( ( for g being Function of VAR ,E holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR ,E holds
( E,g |= H iff F2 . (g . (x. 3)) = g . (x. 4) ) ) implies F1 = F2 )
assume that
A17: for g being Function of VAR ,E holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) and
A18: for g being Function of VAR ,E 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 g = f +* (x. 3),a;
E |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A2, ZF_MODEL:25;
then E,f +* (x. 3),a |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by ZF_MODEL:def 5;
then consider h being Function of VAR ,E such that
A19: for x being Variable st h . x <> (f +* (x. 3),a) . x holds
x. 0 = x and
A20: E,h |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_MODEL:20;
A21: h . (x. 3) = (f +* (x. 3),a) . (x. 3) by A19;
set j = h +* (x. 4),(h . (x. 0 ));
A22: ( (f +* (x. 3),a) . (x. 3) = a & (h +* (x. 4),(h . (x. 0 ))) . (x. 3) = h . (x. 3) ) by FUNCT_7:34, FUNCT_7:130;
( (h +* (x. 4),(h . (x. 0 ))) . (x. 4) = h . (x. 0 ) & (h +* (x. 4),(h . (x. 0 ))) . (x. 0 ) = h . (x. 0 ) ) by FUNCT_7:34, FUNCT_7:130;
then A23: E,h +* (x. 4),(h . (x. 0 )) |= (x. 4) '=' (x. 0 ) by ZF_MODEL:12;
for x being Variable st (h +* (x. 4),(h . (x. 0 ))) . x <> h . x holds
x. 4 = x by FUNCT_7:34;
then E,h +* (x. 4),(h . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A20, ZF_MODEL:16;
then A24: E,h +* (x. 4),(h . (x. 0 )) |= H by A23, ZF_MODEL:19;
then F1 . ((h +* (x. 4),(h . (x. 0 ))) . (x. 3)) = (h +* (x. 4),(h . (x. 0 ))) . (x. 4) by A17;
hence F1 . a = F2 . a by A18, A24, A22, A21; :: thesis: verum