defpred S_{2}[ 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_{3}[ object ] means for g being Function of VAR,E st S_{2}[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_{3}[a] ) )
from XBOOLE_0:sch 1();

( X is Relation-like & X is Function-like )

A25: rng F c= E

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 )

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

( not $1 . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y );

defpred S

E,g |= H;

consider X being set such that

A3: for a being object holds

( a in X iff ( a in [:E,E:] & S

( X is Relation-like & X is Function-like )

proof

then reconsider F = X as Function ;
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_{2}[g +* ((x. 4),b9)]

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_{2}[g +* ((x. 4),c9)]

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;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

proof

for x being Variable st (g +* ((x. 4),b9)) . x <> g . x holds
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;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

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

proof

for x being Variable st (g +* ((x. 4),c9)) . x <> g . x holds
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;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

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

A25: rng F c= E

proof

A27:
E c= dom F
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;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

proof

dom F c= E
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;

then [a9,(h . (x. 0))] in X by A3, A31;

hence a in dom F by FUNCT_1:1; :: thesis: verum

end;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_{2}[f] & f . (x. 3) = [a9,(h . (x. 0))] `1 & f . (x. 4) = [a9,(h . (x. 0))] `2 holds

E,f |= H

[a9,(h . (x. 0))] in [:E,E:]
by ZFMISC_1:87;E,f |= H

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

let f be Function of VAR,E; :: thesis: ( S_{2}[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_{2}[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;

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;let f be Function of VAR,E; :: thesis: ( S

assume that

A32: S

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

for x being Variable st (h +* ((x. 4),(h . (x. 0)))) . x <> h . 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;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

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

then [a9,(h . (x. 0))] in X by A3, A31;

hence a in dom F by FUNCT_1:1; :: thesis: verum

proof

then
E = dom F
by A27;
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;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

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

A53:
( [(f . (x. 3)),(f . (x. 4))] `1 = f . (x. 3) & [(f . (x. 3)),(f . (x. 4))] `2 = f . (x. 4) )
;
assume
E,f |= H
; :: thesis: F . (f . (x. 3)) = f . (x. 4)

then A46: E,f |= All ((x. 0),H) by A1, Th10;

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;then A46: E,f |= All ((x. 0),H) by A1, Th10;

A47: now :: thesis: for g being Function of VAR,E st S_{2}[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

[(f . (x. 3)),(f . (x. 4))] in [:E,E:]
by ZFMISC_1:87;E,g |= H

let g be Function of VAR,E; :: thesis: ( S_{2}[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_{2}[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

end;assume that

A48: S

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

hence
E,g |= H
by A46, ZF_MODEL:16; :: thesis: verumnot 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;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

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

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