let F1, F2 be Function of E,E; ( ( 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) )
; F1 = F2
let a be Element of E; FUNCT_2:def 8 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)));
( (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;
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; verum