set f = the 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 8 :: thesis: F1 . a = F2 . a
set g = the Function of VAR,E +* ((x. 3),a);
E |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_MODEL:23;
then E, the Function of VAR,E +* ((x. 3),a) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) ;
then consider h being Function of VAR,E such that
A19: for x being Variable st h . x <> ( the Function of VAR,E +* ((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) = ( the Function of VAR,E +* ((x. 3),a)) . (x. 3) by A19;
set j = h +* ((x. 4),(h . (x. 0)));
A22: ( ( the Function of VAR,E +* ((x. 3),a)) . (x. 3) = a & (h +* ((x. 4),(h . (x. 0)))) . (x. 3) = h . (x. 3) ) by FUNCT_7:32, FUNCT_7:128;
( (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:32, FUNCT_7:128;
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:32;
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