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
A21: for g being Function of VAR ,E holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) and
A22: 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
consider f being Function of VAR ,E;
set g = f +* (x. 3),a;
A23: (f +* (x. 3),a) . (x. 3) = a by FUNCT_7:130;
E |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A1, 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
A24: ( ( for x being Variable st h . x <> (f +* (x. 3),a) . x holds
x. 0 = x ) & E,h |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) ) by ZF_MODEL:20;
set j = h +* (x. 4),(h . (x. 0 ));
A25: (h +* (x. 4),(h . (x. 0 ))) . (x. 4) = h . (x. 0 ) by FUNCT_7:130;
B25: for x being Variable st x <> x. 4 holds
(h +* (x. 4),(h . (x. 0 ))) . x = h . x by FUNCT_7:34;
then for x being Variable st (h +* (x. 4),(h . (x. 0 ))) . x <> h . x holds
x. 4 = x ;
then A26: E,h +* (x. 4),(h . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A24, ZF_MODEL:16;
(h +* (x. 4),(h . (x. 0 ))) . (x. 0 ) = h . (x. 0 ) by B25;
then E,h +* (x. 4),(h . (x. 0 )) |= (x. 4) '=' (x. 0 ) by A25, ZF_MODEL:12;
then E,h +* (x. 4),(h . (x. 0 )) |= H by A26, ZF_MODEL:19;
then A27: ( F1 . ((h +* (x. 4),(h . (x. 0 ))) . (x. 3)) = (h +* (x. 4),(h . (x. 0 ))) . (x. 4) & F2 . ((h +* (x. 4),(h . (x. 0 ))) . (x. 3)) = (h +* (x. 4),(h . (x. 0 ))) . (x. 4) ) by A21, A22;
( (h +* (x. 4),(h . (x. 0 ))) . (x. 3) = h . (x. 3) & h . (x. 3) = (f +* (x. 3),a) . (x. 3) ) by A24, B25;
hence F1 . a = F2 . a by A23, A27; :: thesis: verum