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

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