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₃[ set ] 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
A2: for a being set 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 set st a in X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def 1 :: thesis: X is Function-like

proof

let a be set ; :: thesis: ( a in X implies ex b, c being set st [b,c] = a )
assume a in X ; :: thesis: ex b, c being set st [b,c] = a
then a in [:E,E:] by A2;
hence ex b, c being set st [b,c] = a by RELAT_1:def 1; :: thesis: verum

end;

let a be set ; :: according to FUNCT_1:def 1 :: thesis: for b₁, b₂ being set holds
( not [a,b₁] in X or not [a,b₂] in X or b₁ = b₂ )
let b, c be set ; :: thesis: ( not [a,b] in X or not [a,c] in X or b = c )
assume A3: ( [a,b] in X & [a,c] in X ) ; :: thesis: b = c
then ( [a,b] in [:E,E:] & [a,c] in [:E,E:] & ( for f being Function of VAR ,E st S₂[f] & f . (x. 3) = [a,b] `1 & f . (x. 4) = [a,b] `2 holds
E,f |= H ) & ( for f being Function of VAR ,E st S₂[f] & f . (x. 3) = [a,c] `1 & f . (x. 4) = [a,c] `2 holds
E,f |= H ) ) by A2;
then reconsider a' = a, b' = b, c' = c as Element of E by ZFMISC_1:106;
A4: ( [a,b] `1 = a' & [a,b] `2 = b' & [a,c] `1 = a' & [a,c] `2 = c' ) by MCART_1:7;
set f = val +* (x. 3),a';
A5: ( (val +* (x. 3),a') . (x. 3) = a' & ( for x being Variable st x <> x. 3 holds
(val +* (x. 3),a') . x = val . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (val +* (x. 3),a') . x <> val . x holds
x = x. 3 by A5;
then E,val +* (x. 3),a' |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A1, ZF_MODEL:16;
then consider g being Function of VAR ,E such that
A6: ( ( for x being Variable st g . x <> (val +* (x. 3),a') . x holds
x. 0 = x ) & E,g |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) ) by ZF_MODEL:20;
set g1 = g +* (x. 4),b';
A7: ( (g +* (x. 4),b') . (x. 4) = b' & ( for x being Variable st x <> x. 4 holds
(g +* (x. 4),b') . x = g . x ) ) by FUNCT_7:34, FUNCT_7:130;
set g2 = g +* (x. 4),c';
A8: ( (g +* (x. 4),c') . (x. 4) = c' & ( for x being Variable st x <> x. 4 holds
(g +* (x. 4),c') . x = g . x ) ) by FUNCT_7:34, FUNCT_7:130;
( ( for x being Variable st (g +* (x. 4),b') . x <> g . x holds
x. 4 = x ) & ( for x being Variable st (g +* (x. 4),c') . x <> g . x holds
x. 4 = x ) ) by A7, A8;
then A9: ( E,g +* (x. 4),b' |= H <=> ((x. 4) '=' (x. 0 )) & E,g +* (x. 4),c' |= H <=> ((x. 4) '=' (x. 0 )) & (g +* (x. 4),b') . (x. 3) = g . (x. 3) & (g +* (x. 4),c') . (x. 3) = g . (x. 3) & g . (x. 3) = (val +* (x. 3),a') . (x. 3) ) by A6, ZF_MODEL:16;
A10: S₂[g +* (x. 4),b']

proof

let y be Variable; :: thesis: ( not (g +* (x. 4),b') . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A11: (g +* (x. 4),b') . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume ( x. 0 <> y & x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
then ( (val +* (x. 3),a') . y = val . y & g . y = (val +* (x. 3),a') . y & (g +* (x. 4),b') . y = g . y ) by A5, A6, A7;
hence contradiction by A11; :: thesis: verum

end;

S₂[g +* (x. 4),c']

proof

let y be Variable; :: thesis: ( not (g +* (x. 4),c') . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A12: (g +* (x. 4),c') . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume ( x. 0 <> y & x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
then ( (val +* (x. 3),a') . y = val . y & g . y = (val +* (x. 3),a') . y & (g +* (x. 4),c') . y = g . y ) by A5, A6, A8;
hence contradiction by A12; :: thesis: verum

end;

then ( E,g +* (x. 4),b' |= H & E,g +* (x. 4),c' |= H ) by A2, A3, A4, A5, A7, A8, A9, A10;
then ( E,g +* (x. 4),b' |= (x. 4) '=' (x. 0 ) & E,g +* (x. 4),c' |= (x. 4) '=' (x. 0 ) ) by A9, ZF_MODEL:19;
then ( (g +* (x. 4),b') . (x. 4) = (g +* (x. 4),b') . (x. 0 ) & (g +* (x. 4),c') . (x. 4) = (g +* (x. 4),c') . (x. 0 ) & (g +* (x. 4),b') . (x. 0 ) = g . (x. 0 ) & (g +* (x. 4),c') . (x. 0 ) = g . (x. 0 ) ) by A7, A8, ZF_MODEL:12;
hence b = c by A7, A8; :: thesis: verum

end;

then reconsider F = X as Function ;
A13: E = dom F

proof

thus E c= dom F :: according to XBOOLE_0:def 10 :: thesis: dom F c= E

proof

let a be set ; :: 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 a' = a as Element of E ;
set g = val +* (x. 3),a';
A14: ( (val +* (x. 3),a') . (x. 3) = a' & ( for x being Variable st x <> x. 3 holds
(val +* (x. 3),a') . x = val . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (val +* (x. 3),a') . x <> val . x holds
x = x. 3 by A14;
then E,val +* (x. 3),a' |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A1, ZF_MODEL:16;
then consider h being Function of VAR ,E such that
A15: ( ( for x being Variable st h . x <> (val +* (x. 3),a') . x holds
x = x. 0 ) & E,h |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) ) by ZF_MODEL:20;
set u = h . (x. 0 );
A16: [a',(h . (x. 0 ))] in [:E,E:] by ZFMISC_1:106;

now

let f be Function of VAR ,E; :: thesis: ( S₂[f] & f . (x. 3) = [a',(h . (x. 0 ))] `1 & f . (x. 4) = [a',(h . (x. 0 ))] `2 implies E,f |= H )
assume A17: ( S₂[f] & f . (x. 3) = [a',(h . (x. 0 ))] `1 & f . (x. 4) = [a',(h . (x. 0 ))] `2 ) ; :: thesis: E,f |= H
set m = h +* (x. 4),(h . (x. 0 ));
A18: ( (h +* (x. 4),(h . (x. 0 ))) . (x. 4) = h . (x. 0 ) & ( for x being Variable st x <> x. 4 holds
(h +* (x. 4),(h . (x. 0 ))) . x = h . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (h +* (x. 4),(h . (x. 0 ))) . x <> h . x holds
x. 4 = x by A18;
then A19: E,h +* (x. 4),(h . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A15, ZF_MODEL:16;
(h +* (x. 4),(h . (x. 0 ))) . (x. 0 ) = h . (x. 0 ) by A18;
then E,h +* (x. 4),(h . (x. 0 )) |= (x. 4) '=' (x. 0 ) by A18, ZF_MODEL:12;
then E,h +* (x. 4),(h . (x. 0 )) |= H by A19, ZF_MODEL:19;
then A20: E,h +* (x. 4),(h . (x. 0 )) |= All (x. 0 ),H by A1, Th10;

now

let x be Variable; :: thesis: ( f . x <> (h +* (x. 4),(h . (x. 0 ))) . x implies not x. 0 <> x )
assume A21: f . x <> (h +* (x. 4),(h . (x. 0 ))) . x ; :: thesis: not x. 0 <> x
assume A22: x. 0 <> x ; :: thesis: contradiction
( (val +* (x. 3),a') . (x. 3) = h . (x. 3) & h . (x. 3) = (h +* (x. 4),(h . (x. 0 ))) . (x. 3) ) by A15, A18;
then ( x <> x. 4 & x <> x. 3 ) by A14, A17, A18, A21, MCART_1:7;
then ( f . x = val . x & (val +* (x. 3),a') . x = val . x & h . x = (val +* (x. 3),a') . x & (h +* (x. 4),(h . (x. 0 ))) . x = h . x ) by A14, A15, A17, A18, A22;
hence contradiction by A21; :: thesis: verum

end;

hence E,f |= H by A20, ZF_MODEL:16; :: thesis: verum

end;

then [a',(h . (x. 0 ))] in X by A2, A16;
hence a in dom F by FUNCT_1:8; :: thesis: verum

end;

thus dom F c= E :: thesis: verum

proof

let a be set ; :: 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 set such that
A23: [a,b] in F by RELAT_1:def 4;
[a,b] in [:E,E:] by A2, A23;
hence a in E by ZFMISC_1:106; :: thesis: verum

end;

end;

rng F c= E

proof

let b be set ; :: 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 set such that
A24: ( a in dom F & b = F . a ) by FUNCT_1:def 5;
[a,b] in F by A24, FUNCT_1:8;
then [a,b] in [:E,E:] by A2;
hence b in E by ZFMISC_1:106; :: thesis: verum

end;

then reconsider F = F as Function of E,E by A13, FUNCT_2:def 1, RELSET_1:11;
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 A25: 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) )
A26: ( [(f . (x. 3)),(f . (x. 4))] `1 = f . (x. 3) & [(f . (x. 3)),(f . (x. 4))] `2 = f . (x. 4) ) by MCART_1:7;
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 A27: E,f |= All (x. 0 ),H by A1, Th10;
A28: [(f . (x. 3)),(f . (x. 4))] in [:E,E:] by ZFMISC_1:106;

now

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 A29: ( S₂[g] & 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

let x be Variable; :: thesis: ( g . x <> f . x implies not x. 0 <> x )
assume that
A30: g . x <> f . x and
A31: x. 0 <> x ; :: thesis: contradiction
( x <> x. 3 & x <> x. 4 ) by A29, A30, MCART_1:7;
then ( f . x = val . x & g . x = val . x ) by A25, A29, A31;
hence contradiction by A30; :: thesis: verum

end;

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

end;

then [(f . (x. 3)),(f . (x. 4))] in X by A2, A28;
hence F . (f . (x. 3)) = f . (x. 4) by FUNCT_1:8; :: thesis: verum

end;

A32: ( f . (x. 3) in E & 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 A32, FUNCT_1:8;
hence E,f |= H by A2, A25, A26; :: thesis: verum