defpred S₂[ Function of VAR,E] means for y being Variable holds
( not $1 . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y );
defpred S₃[ object ] means for g being Function of VAR,E st S₂[g] & g . (x. 3) = $1 `1 & g . (x. 4) = $1 `2 holds
E,g |= H;
consider X being set such that
A3: for a being object holds
( a in X iff ( a in [:E,E:] & S₃[a] ) ) from XBOOLE_0:sch 1();
( X is Relation-like & X is Function-like )

proof

thus for a being object st a in X holds
ex b, c being object st [b,c] = a by A3, RELAT_1:def 1; :: according to RELAT_1:def 1 :: thesis: X is Function-like
let a, b, c be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [a,b] in X or not [a,c] in X or b = c )
assume that
A4: [a,b] in X and
A5: [a,c] in X ; :: thesis: b = c
( [a,b] in [:E,E:] & [a,c] in [:E,E:] ) by A3, A4, A5;
then reconsider a9 = a, b9 = b, c9 = c as Element of E by ZFMISC_1:87;
set f = val +* ((x. 3),a9);
for x being Variable st (val +* ((x. 3),a9)) . x <> val . x holds
x = x. 3 by FUNCT_7:32;
then E,val +* ((x. 3),a9) |= 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
A6: for x being Variable st g . x <> (val +* ((x. 3),a9)) . x holds
x. 0 = x and
A7: E,g |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;
A8: ( (val +* ((x. 3),a9)) . (x. 3) = a9 & g . (x. 3) = (val +* ((x. 3),a9)) . (x. 3) ) by A6, FUNCT_7:128;
set g1 = g +* ((x. 4),b9);
A9: (g +* ((x. 4),b9)) . (x. 4) = b9 by FUNCT_7:128;
A10: S₂[g +* ((x. 4),b9)]

proof

let y be Variable; :: thesis: ( not (g +* ((x. 4),b9)) . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A11: (g +* ((x. 4),b9)) . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume that
A12: x. 0 <> y and
A13: ( x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
( (val +* ((x. 3),a9)) . y = val . y & (g +* ((x. 4),b9)) . y = g . y ) by A13, FUNCT_7:32;
hence contradiction by A6, A11, A12; :: thesis: verum

end;

for x being Variable st (g +* ((x. 4),b9)) . x <> g . x holds
x. 4 = x by FUNCT_7:32;
then A14: E,g +* ((x. 4),b9) |= H <=> ((x. 4) '=' (x. 0)) by A7, ZF_MODEL:16;
A15: (g +* ((x. 4),b9)) . (x. 3) = g . (x. 3) by FUNCT_7:32;
( [a,b] `1 = a9 & [a,b] `2 = b9 ) ;
then E,g +* ((x. 4),b9) |= H by A3, A4, A9, A15, A8, A10;
then E,g +* ((x. 4),b9) |= (x. 4) '=' (x. 0) by A14, ZF_MODEL:19;
then A16: (g +* ((x. 4),b9)) . (x. 4) = (g +* ((x. 4),b9)) . (x. 0) by ZF_MODEL:12;
set g2 = g +* ((x. 4),c9);
A17: (g +* ((x. 4),c9)) . (x. 4) = c9 by FUNCT_7:128;
A18: S₂[g +* ((x. 4),c9)]

proof

let y be Variable; :: thesis: ( not (g +* ((x. 4),c9)) . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A19: (g +* ((x. 4),c9)) . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume that
A20: x. 0 <> y and
A21: ( x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
( (val +* ((x. 3),a9)) . y = val . y & (g +* ((x. 4),c9)) . y = g . y ) by A21, FUNCT_7:32;
hence contradiction by A6, A19, A20; :: thesis: verum

end;

for x being Variable st (g +* ((x. 4),c9)) . x <> g . x holds
x. 4 = x by FUNCT_7:32;
then A22: E,g +* ((x. 4),c9) |= H <=> ((x. 4) '=' (x. 0)) by A7, ZF_MODEL:16;
A23: (g +* ((x. 4),c9)) . (x. 3) = g . (x. 3) by FUNCT_7:32;
( [a,c] `1 = a9 & [a,c] `2 = c9 ) ;
then E,g +* ((x. 4),c9) |= H by A3, A5, A17, A23, A8, A18;
then A24: E,g +* ((x. 4),c9) |= (x. 4) '=' (x. 0) by A22, ZF_MODEL:19;
( (g +* ((x. 4),b9)) . (x. 0) = g . (x. 0) & (g +* ((x. 4),c9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;
hence b = c by A9, A17, A24, A16, ZF_MODEL:12; :: thesis: verum

end;

then reconsider F = X as Function ;
A25: rng F c= E

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng F or b in E )
assume b in rng F ; :: thesis: b in E
then consider a being object such that
A26: ( a in dom F & b = F . a ) by FUNCT_1:def 3;
[a,b] in F by A26, FUNCT_1:1;
then [a,b] in [:E,E:] by A3;
hence b in E by ZFMISC_1:87; :: thesis: verum

end;

A27: E c= dom F

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in dom F )
assume a in E ; :: thesis: a in dom F
then reconsider a9 = a as Element of E ;
set g = val +* ((x. 3),a9);
for x being Variable st (val +* ((x. 3),a9)) . x <> val . x holds
x = x. 3 by FUNCT_7:32;
then E,val +* ((x. 3),a9) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_MODEL:16;
then consider h being Function of VAR,E such that
A28: for x being Variable st h . x <> (val +* ((x. 3),a9)) . x holds
x = x. 0 and
A29: E,h |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;
set u = h . (x. 0);
A30: (val +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;

A31: now :: thesis: for f being Function of VAR,E st S₂[f] & f . (x. 3) = [a9,(h . (x. 0))] `1 & f . (x. 4) = [a9,(h . (x. 0))] `2 holds
E,f |= H

set m = h +* ((x. 4),(h . (x. 0)));
let f be Function of VAR,E; :: thesis: ( S₂[f] & f . (x. 3) = [a9,(h . (x. 0))] `1 & f . (x. 4) = [a9,(h . (x. 0))] `2 implies E,f |= H )
assume that
A32: S₂[f] and
A33: f . (x. 3) = [a9,(h . (x. 0))] `1 and
A34: f . (x. 4) = [a9,(h . (x. 0))] `2 ; :: thesis: E,f |= H
A35: (h +* ((x. 4),(h . (x. 0)))) . (x. 4) = h . (x. 0) by FUNCT_7:128;

A36: now :: thesis: for x being Variable st f . x <> (h +* ((x. 4),(h . (x. 0)))) . x holds
not x. 0 <> x

let x be Variable; :: thesis: ( f . x <> (h +* ((x. 4),(h . (x. 0)))) . x implies not x. 0 <> x )
assume A37: f . x <> (h +* ((x. 4),(h . (x. 0)))) . x ; :: thesis: not x. 0 <> x
A38: x <> x. 4 by A34, A35, A37;
then A39: (h +* ((x. 4),(h . (x. 0)))) . x = h . x by FUNCT_7:32;
( (val +* ((x. 3),a9)) . (x. 3) = h . (x. 3) & h . (x. 3) = (h +* ((x. 4),(h . (x. 0)))) . (x. 3) ) by A28, FUNCT_7:32;
then A40: x <> x. 3 by A30, A33, A37;
then A41: (val +* ((x. 3),a9)) . x = val . x by FUNCT_7:32;
assume A42: x. 0 <> x ; :: thesis: contradiction
then f . x = val . x by A32, A38, A40;
hence contradiction by A28, A37, A42, A41, A39; :: thesis: verum

end;

for x being Variable st (h +* ((x. 4),(h . (x. 0)))) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then A43: E,h +* ((x. 4),(h . (x. 0))) |= H <=> ((x. 4) '=' (x. 0)) by A29, ZF_MODEL:16;
(h +* ((x. 4),(h . (x. 0)))) . (x. 0) = h . (x. 0) by FUNCT_7:32;
then E,h +* ((x. 4),(h . (x. 0))) |= (x. 4) '=' (x. 0) by A35, ZF_MODEL:12;
then E,h +* ((x. 4),(h . (x. 0))) |= H by A43, ZF_MODEL:19;
then E,h +* ((x. 4),(h . (x. 0))) |= All ((x. 0),H) by A1, Th10;
hence E,f |= H by A36, ZF_MODEL:16; :: thesis: verum

end;

[a9,(h . (x. 0))] in [:E,E:] by ZFMISC_1:87;
then [a9,(h . (x. 0))] in X by A3, A31;
hence a in dom F by FUNCT_1:1; :: thesis: verum

end;

dom F c= E

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom F or a in E )
assume a in dom F ; :: thesis: a in E
then consider b being object such that
A44: [a,b] in F by XTUPLE_0:def 12;
[a,b] in [:E,E:] by A3, A44;
hence a in E by ZFMISC_1:87; :: thesis: verum

end;

then E = dom F by A27;
then reconsider F = F as Function of E,E by A25, FUNCT_2:def 1, RELSET_1:4;
take F ; :: 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 F . (g . (x. 3)) = g . (x. 4) )
let f be Function of VAR,E; :: thesis: ( ( for y being Variable holds
( not f . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) implies ( E,f |= H iff F . (f . (x. 3)) = f . (x. 4) ) )
assume A45: for y being Variable holds
( not f . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ; :: thesis: ( E,f |= H iff F . (f . (x. 3)) = f . (x. 4) )
thus ( E,f |= H implies F . (f . (x. 3)) = f . (x. 4) ) :: thesis: ( F . (f . (x. 3)) = f . (x. 4) implies E,f |= H )

proof

assume E,f |= H ; :: thesis: F . (f . (x. 3)) = f . (x. 4)
then A46: E,f |= All ((x. 0),H) by A1, Th10;

A47: now :: thesis: for g being Function of VAR,E st S₂[g] & g . (x. 3) = [(f . (x. 3)),(f . (x. 4))] `1 & g . (x. 4) = [(f . (x. 3)),(f . (x. 4))] `2 holds
E,g |= H

let g be Function of VAR,E; :: thesis: ( S₂[g] & g . (x. 3) = [(f . (x. 3)),(f . (x. 4))] `1 & g . (x. 4) = [(f . (x. 3)),(f . (x. 4))] `2 implies E,g |= H )
assume that
A48: S₂[g] and
A49: ( g . (x. 3) = [(f . (x. 3)),(f . (x. 4))] `1 & g . (x. 4) = [(f . (x. 3)),(f . (x. 4))] `2 ) ; :: thesis: E,g |= H

now :: thesis: for x being Variable st g . x <> f . x holds
not x. 0 <> x

let x be Variable; :: thesis: ( g . x <> f . x implies not x. 0 <> x )
assume that
A50: g . x <> f . x and
A51: x. 0 <> x ; :: thesis: contradiction
A52: ( x <> x. 3 & x <> x. 4 ) by A49, A50;
then f . x = val . x by A45, A51;
hence contradiction by A48, A50, A51, A52; :: thesis: verum

end;

hence E,g |= H by A46, ZF_MODEL:16; :: thesis: verum

end;

[(f . (x. 3)),(f . (x. 4))] in [:E,E:] by ZFMISC_1:87;
then [(f . (x. 3)),(f . (x. 4))] in X by A3, A47;
hence F . (f . (x. 3)) = f . (x. 4) by FUNCT_1:1; :: thesis: verum

end;

A53: ( [(f . (x. 3)),(f . (x. 4))] `1 = f . (x. 3) & [(f . (x. 3)),(f . (x. 4))] `2 = f . (x. 4) ) ;
A54: dom F = E by FUNCT_2:def 1;
assume F . (f . (x. 3)) = f . (x. 4) ; :: thesis: E,f |= H
then [(f . (x. 3)),(f . (x. 4))] in F by A54, FUNCT_1:1;
hence E,f |= H by A3, A45, A53; :: thesis: verum