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

A55: 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

A56: 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 8 :: thesis: F1 . a = F2 . a

set f = val +* ((x. 3),a);

for x being Variable st (val +* ((x. 3),a)) . x <> val . x holds

x. 3 = x by FUNCT_7:32;

then E,val +* ((x. 3),a) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_MODEL:16;

then consider g being Function of VAR,E such that

A57: for x being Variable st g . x <> (val +* ((x. 3),a)) . x holds

x. 0 = x and

A58: E,g |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;

A59: g . (x. 3) = (val +* ((x. 3),a)) . (x. 3) by A57;

set h = g +* ((x. 4),(g . (x. 0)));

then A63: E,g +* ((x. 4),(g . (x. 0))) |= (x. 4) '=' (x. 0) by ZF_MODEL:12;

A64: ( (val +* ((x. 3),a)) . (x. 3) = a & (g +* ((x. 4),(g . (x. 0)))) . (x. 3) = g . (x. 3) ) by FUNCT_7:32, FUNCT_7:128;

for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> g . x holds

x. 4 = x by FUNCT_7:32;

then E,g +* ((x. 4),(g . (x. 0))) |= H <=> ((x. 4) '=' (x. 0)) by A58, ZF_MODEL:16;

then A65: E,g +* ((x. 4),(g . (x. 0))) |= H by A63, ZF_MODEL:19;

then F1 . ((g +* ((x. 4),(g . (x. 0)))) . (x. 3)) = (g +* ((x. 4),(g . (x. 0)))) . (x. 4) by A55, A60;

hence F1 . a = F2 . a by A56, A65, A60, A64, A59; :: thesis: verum

( 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

A55: 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

A56: 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 8 :: thesis: F1 . a = F2 . a

set f = val +* ((x. 3),a);

for x being Variable st (val +* ((x. 3),a)) . x <> val . x holds

x. 3 = x by FUNCT_7:32;

then E,val +* ((x. 3),a) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_MODEL:16;

then consider g being Function of VAR,E such that

A57: for x being Variable st g . x <> (val +* ((x. 3),a)) . x holds

x. 0 = x and

A58: E,g |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;

A59: g . (x. 3) = (val +* ((x. 3),a)) . (x. 3) by A57;

set h = g +* ((x. 4),(g . (x. 0)));

A60: now :: thesis: for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x & x. 3 <> x holds

not x. 4 <> x

( (g +* ((x. 4),(g . (x. 0)))) . (x. 4) = g . (x. 0) & (g +* ((x. 4),(g . (x. 0)))) . (x. 0) = g . (x. 0) )
by FUNCT_7:32, FUNCT_7:128;not x. 4 <> x

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

A61: ( (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x ) and

A62: ( x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction

( (val +* ((x. 3),a)) . x = val . x & (g +* ((x. 4),(g . (x. 0)))) . x = g . x ) by A62, FUNCT_7:32;

hence contradiction by A57, A61; :: thesis: verum

end;assume that

A61: ( (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x ) and

A62: ( x. 3 <> x & x. 4 <> x ) ; :: thesis: contradiction

( (val +* ((x. 3),a)) . x = val . x & (g +* ((x. 4),(g . (x. 0)))) . x = g . x ) by A62, FUNCT_7:32;

hence contradiction by A57, A61; :: thesis: verum

then A63: E,g +* ((x. 4),(g . (x. 0))) |= (x. 4) '=' (x. 0) by ZF_MODEL:12;

A64: ( (val +* ((x. 3),a)) . (x. 3) = a & (g +* ((x. 4),(g . (x. 0)))) . (x. 3) = g . (x. 3) ) by FUNCT_7:32, FUNCT_7:128;

for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> g . x holds

x. 4 = x by FUNCT_7:32;

then E,g +* ((x. 4),(g . (x. 0))) |= H <=> ((x. 4) '=' (x. 0)) by A58, ZF_MODEL:16;

then A65: E,g +* ((x. 4),(g . (x. 0))) |= H by A63, ZF_MODEL:19;

then F1 . ((g +* ((x. 4),(g . (x. 0)))) . (x. 3)) = (g +* ((x. 4),(g . (x. 0)))) . (x. 4) by A55, A60;

hence F1 . a = F2 . a by A56, A65, A60, A64, A59; :: thesis: verum