let E be non empty set ; :: thesis:
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def 2 :: thesis:

A2: now

assume A3: for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ; :: thesis:
let H be ZF-formula; :: thesis:
let f be Function of VAR ,E; :: thesis:
assume that
A4: {(x. 0 ),(x. 1),(x. 2)} misses Free H and
A5: E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis:
x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A6: not x. 0 in Free H by A4, XBOOLE_0:3;

now

let a be set ; :: thesis:
assume a in {(x. 1),(x. 2)} ; :: thesis:
then ( a = x. 1 or a = x. 2 ) by TARSKI:def 2;
then a in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
hence not a in Free H by A4, XBOOLE_0:3; :: thesis:

end;

then A7: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
let u be Element of E; :: thesis:
E |= the_axiom_of_substitution_for H by A3, A4;
then ( E,f |= the_axiom_of_substitution_for H & the_axiom_of_substitution_for H = (All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)))))) ) by ZF_MODEL:def 5;
then A8: E,f |= All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))))) by A5, ZF_MODEL:18;
set g = f +* (x. 1),u;
A9: ( (f +* (x. 1),u) . (x. 1) = u & ( for x being Variable st x <> x. 1 holds
(f +* (x. 1),u) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (f +* (x. 1),u) . x <> f . x holds
x. 1 = x by A9;
then E,f +* (x. 1),u |= Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)))) by A8, ZF_MODEL:16;
then consider h being Function of VAR ,E such that
A10: ( ( for x being Variable st h . x <> (f +* (x. 1),u) . x holds
x. 2 = x ) & E,h |= All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))) ) by ZF_MODEL:20;
set v = h . (x. 2);
A11: (def_func' H,f) .: u c= h . (x. 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A12: a in (def_func' H,f) .: u ; :: thesis:
then consider b being set such that
A13: ( b in dom (def_func' H,f) & b in u & (def_func' H,f) . b = a ) by FUNCT_1:def 12;
reconsider e = a as Element of E by A12;
reconsider b = b as Element of E by A13;
set i = h +* (x. 4),e;
A14: ( (h +* (x. 4),e) . (x. 4) = e & ( for x being Variable st x <> x. 4 holds
(h +* (x. 4),e) . x = h . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (h +* (x. 4),e) . x <> h . x holds
x. 4 = x by A14;
then A15: E,h +* (x. 4),e |= ((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A10, ZF_MODEL:16;
set j = (h +* (x. 4),e) +* (x. 3),b;
A16: ( ((h +* (x. 4),e) +* (x. 3),b) . (x. 3) = b & ( for x being Variable st x <> x. 3 holds
((h +* (x. 4),e) +* (x. 3),b) . x = (h +* (x. 4),e) . x ) ) by FUNCT_7:34, FUNCT_7:130;
( ((h +* (x. 4),e) +* (x. 3),b) . (x. 1) = (h +* (x. 4),e) . (x. 1) & (h +* (x. 4),e) . (x. 1) = h . (x. 1) & h . (x. 1) = (f +* (x. 1),u) . (x. 1) ) by A10, A14, A16;
then A17: E,(h +* (x. 4),e) +* (x. 3),b |= (x. 3) 'in' (x. 1) by A9, A13, A16, ZF_MODEL:13;
set m1 = f +* (x. 3),b;
A18: ( (f +* (x. 3),b) . (x. 3) = b & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),b) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set m = (f +* (x. 3),b) +* (x. 4),e;
A19: ( ((f +* (x. 3),b) +* (x. 4),e) . (x. 4) = e & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),b) +* (x. 4),e) . x = (f +* (x. 3),b) . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let y be Variable; :: thesis:
assume A20: ((f +* (x. 3),b) +* (x. 4),e) . y <> f . y ; :: thesis:
assume ( x. 0 <> y & x. 3 <> y & x. 4 <> y ) ; :: thesis:
then ( ((f +* (x. 3),b) +* (x. 4),e) . y = (f +* (x. 3),b) . y & (f +* (x. 3),b) . y = f . y ) by A18, A19;
hence contradiction by A20; :: thesis:

end;

then A21: ( E,(f +* (x. 3),b) +* (x. 4),e |= H iff (def_func' H,f) . (((f +* (x. 3),b) +* (x. 4),e) . (x. 3)) = ((f +* (x. 3),b) +* (x. 4),e) . (x. 4) ) by A5, A6, Def1;
A22: ((f +* (x. 3),b) +* (x. 4),e) . (x. 3) = (f +* (x. 3),b) . (x. 3) by A19;
A23: E,(f +* (x. 3),b) +* (x. 4),e |= All (x. 1),(x. 2),H by A7, A13, A18, A19, A21, Th11;
set k = ((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1));
A24: ( (((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . (x. 1) = ((h +* (x. 4),e) +* (x. 3),b) . (x. 1) & ( for x being Variable st x <> x. 1 holds
(((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . x = ((f +* (x. 3),b) +* (x. 4),e) . x ) ) by FUNCT_7:34, FUNCT_7:130;
( All (x. 1),(x. 2),H = All (x. 1),(All (x. 2),H) & ( for x being Variable st (((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . x <> ((f +* (x. 3),b) +* (x. 4),e) . x holds
x. 1 = x ) ) by A24;
then A25: E,((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1)) |= All (x. 2),H by A23, ZF_MODEL:16;

now

let x be Variable; :: thesis:
assume that
A26: ((h +* (x. 4),e) +* (x. 3),b) . x <> (((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . x and
A27: x. 2 <> x ; :: thesis:
A28: x <> x. 1 by A24, A26;
A29: x <> x. 3 by A16, A18, A22, A24, A26;
( (((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . (x. 4) = ((f +* (x. 3),b) +* (x. 4),e) . (x. 4) & ((h +* (x. 4),e) +* (x. 3),b) . (x. 4) = (h +* (x. 4),e) . (x. 4) ) by A16, A24;
then A30: x <> x. 4 by A14, A19, A26;
(((f +* (x. 3),b) +* (x. 4),e) +* (x. 1),(((h +* (x. 4),e) +* (x. 3),b) . (x. 1))) . x = ((f +* (x. 3),b) +* (x. 4),e) . x by A24, A28
.= (f +* (x. 3),b) . x by A19, A30
.= f . x by A18, A29
.= (f +* (x. 1),u) . x by A9, A28
.= h . x by A10, A27
.= (h +* (x. 4),e) . x by A14, A30
.= ((h +* (x. 4),e) +* (x. 3),b) . x by A16, A29 ;
hence contradiction by A26; :: thesis:

end;

then E,(h +* (x. 4),e) +* (x. 3),b |= H by A25, ZF_MODEL:16;
then A31: E,(h +* (x. 4),e) +* (x. 3),b |= ((x. 3) 'in' (x. 1)) '&' H by A17, ZF_MODEL:15;
for x being Variable st (h +* (x. 4),e) . x <> ((h +* (x. 4),e) +* (x. 3),b) . x holds
x. 3 = x by A16;
then E,h +* (x. 4),e |= Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H) by A31, ZF_MODEL:20;
then E,h +* (x. 4),e |= (x. 4) 'in' (x. 2) by A15, ZF_MODEL:19;
then ( (h +* (x. 4),e) . (x. 4) in (h +* (x. 4),e) . (x. 2) & (h +* (x. 4),e) . (x. 2) = h . (x. 2) ) by A14, ZF_MODEL:13;
hence a in h . (x. 2) by A14; :: thesis:

end;

h . (x. 2) c= (def_func' H,f) .: u

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A32: a in h . (x. 2) ; :: thesis:
h . (x. 2) c= E by A1;
then reconsider e = a as Element of E by A32;
set i = h +* (x. 4),e;
A33: ( (h +* (x. 4),e) . (x. 4) = e & ( for x being Variable st x <> x. 4 holds
(h +* (x. 4),e) . x = h . x ) ) by FUNCT_7:34, FUNCT_7:130;
for x being Variable st (h +* (x. 4),e) . x <> h . x holds
x. 4 = x by A33;
then A34: E,h +* (x. 4),e |= ((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A10, ZF_MODEL:16;
(h +* (x. 4),e) . (x. 2) = h . (x. 2) by A33;
then E,h +* (x. 4),e |= (x. 4) 'in' (x. 2) by A32, A33, ZF_MODEL:13;
then E,h +* (x. 4),e |= Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H) by A34, ZF_MODEL:19;
then consider j being Function of VAR ,E such that
A35: ( ( for x being Variable st j . x <> (h +* (x. 4),e) . x holds
x. 3 = x ) & E,j |= ((x. 3) 'in' (x. 1)) '&' H ) by ZF_MODEL:20;
A36: ( E,j |= (x. 3) 'in' (x. 1) & E,j |= H ) by A35, ZF_MODEL:15;
then A37: ( j . (x. 3) in j . (x. 1) & j . (x. 1) = (h +* (x. 4),e) . (x. 1) & (h +* (x. 4),e) . (x. 1) = h . (x. 1) & h . (x. 1) = (f +* (x. 1),u) . (x. 1) ) by A10, A33, A35, ZF_MODEL:13;
set m1 = f +* (x. 3),(j . (x. 3));
A38: ( (f +* (x. 3),(j . (x. 3))) . (x. 3) = j . (x. 3) & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),(j . (x. 3))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set m = (f +* (x. 3),(j . (x. 3))) +* (x. 4),e;
A39: ( ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 4) = e & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . x = (f +* (x. 3),(j . (x. 3))) . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let y be Variable; :: thesis:
assume A40: ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . y <> f . y ; :: thesis:
assume ( x. 0 <> y & x. 3 <> y & x. 4 <> y ) ; :: thesis:
then ( ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . y = (f +* (x. 3),(j . (x. 3))) . y & (f +* (x. 3),(j . (x. 3))) . y = f . y ) by A38, A39;
hence contradiction by A40; :: thesis:

end;

then A41: ( E,(f +* (x. 3),(j . (x. 3))) +* (x. 4),e |= H iff (def_func' H,f) . (((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 3)) = ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 4) ) by A5, A6, Def1;
A42: E,j |= All (x. 1),(x. 2),H by A7, A36, Th11;
set k = j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1));
A43: ( (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . (x. 1) = ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1) & ( for x being Variable st x <> x. 1 holds
(j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . x = j . x ) ) by FUNCT_7:34, FUNCT_7:130;
( All (x. 1),(x. 2),H = All (x. 1),(All (x. 2),H) & ( for x being Variable st (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . x <> j . x holds
x. 1 = x ) ) by A43;
then A44: E,j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1)) |= All (x. 2),H by A42, ZF_MODEL:16;

now

let x be Variable; :: thesis:
assume that
A45: ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . x <> (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . x and
A46: x. 2 <> x ; :: thesis:
A47: x. 1 <> x by A43, A45;
( (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . (x. 3) = j . (x. 3) & (f +* (x. 3),(j . (x. 3))) . (x. 3) = ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 3) ) by A39, A43;
then A48: x. 3 <> x by A38, A45;
( (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . (x. 4) = j . (x. 4) & j . (x. 4) = (h +* (x. 4),e) . (x. 4) ) by A35, A43;
then A49: x. 4 <> x by A33, A39, A45;
(j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . (x. 1))) . x = j . x by A43, A47
.= (h +* (x. 4),e) . x by A35, A48
.= h . x by A33, A49
.= (f +* (x. 1),u) . x by A10, A46
.= f . x by A9, A47
.= (f +* (x. 3),(j . (x. 3))) . x by A38, A48
.= ((f +* (x. 3),(j . (x. 3))) +* (x. 4),e) . x by A39, A49 ;
hence contradiction by A45; :: thesis:

end;

then A50: (def_func' H,f) . (j . (x. 3)) = a by A38, A39, A41, A44, ZF_MODEL:16;
( j . (x. 3) in E & dom (def_func' H,f) = E ) by FUNCT_2:def 1;
hence a in (def_func' H,f) .: u by A9, A37, A50, FUNCT_1:def 12; :: thesis:

end;

then (def_func' H,f) .: u = h . (x. 2) by A11, XBOOLE_0:def 10;
hence (def_func' H,f) .: u in E ; :: thesis:

end;

now

assume A51: for H being ZF-formula
for f being Function of VAR ,E st {(x. 0 ),(x. 1),(x. 2)} misses Free H & E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for u being Element of E holds (def_func' H,f) .: u in E ; :: thesis:
let H be ZF-formula; :: thesis:
assume A52: {(x. 0 ),(x. 1),(x. 2)} misses Free H ; :: thesis:
x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A53: not x. 0 in Free H by A52, XBOOLE_0:3;

now

end;

then A54: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
thus E |= the_axiom_of_substitution_for H :: thesis:

proof

let f be Function of VAR ,E; :: according to ZF_MODEL:def 5 :: thesis:

now

assume A55: E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis:

now

let g be Function of VAR ,E; :: thesis:
assume A56: for x being Variable st g . x <> f . x holds
x. 1 = x ; :: thesis:
reconsider v = (def_func' H,f) .: (g . (x. 1)) as Element of E by A51, A52, A55;
set h = g +* (x. 2),v;
A57: ( (g +* (x. 2),v) . (x. 2) = v & ( for x being Variable st x <> x. 2 holds
(g +* (x. 2),v) . x = g . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let i be Function of VAR ,E; :: thesis:
assume A58: for x being Variable st i . x <> (g +* (x. 2),v) . x holds
x. 4 = x ; :: thesis:

A59: now

assume E,i |= (x. 4) 'in' (x. 2) ; :: thesis:
then ( i . (x. 4) in i . (x. 2) & i . (x. 2) = (g +* (x. 2),v) . (x. 2) ) by A58, ZF_MODEL:13;
then consider a being set such that
A60: ( a in dom (def_func' H,f) & a in g . (x. 1) & i . (x. 4) = (def_func' H,f) . a ) by A57, FUNCT_1:def 12;
reconsider a = a as Element of E by A60;
set j = i +* (x. 3),a;
A61: ( (i +* (x. 3),a) . (x. 3) = a & ( for x being Variable st x <> x. 3 holds
(i +* (x. 3),a) . x = i . x ) ) by FUNCT_7:34, FUNCT_7:130;
( (i +* (x. 3),a) . (x. 1) = i . (x. 1) & i . (x. 1) = (g +* (x. 2),v) . (x. 1) & (g +* (x. 2),v) . (x. 1) = g . (x. 1) ) by A57, A58, A61;
then A62: E,i +* (x. 3),a |= (x. 3) 'in' (x. 1) by A60, A61, ZF_MODEL:13;
set m1 = f +* (x. 3),((i +* (x. 3),a) . (x. 3));
A63: ( (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . (x. 3) = (i +* (x. 3),a) . (x. 3) & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set m = (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4));
A64: ( ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) = i . (x. 4) & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x = (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . x ) ) by FUNCT_7:34, FUNCT_7:130;

now

let x be Variable; :: thesis:
assume that
A65: ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x <> f . x and
A66: ( x. 0 <> x & x. 3 <> x & x. 4 <> x ) ; :: thesis:
( ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x = (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . x & (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . x = f . x ) by A63, A64, A66;
hence contradiction by A65; :: thesis:

end;

then ( ( E,(f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4)) |= H implies (def_func' H,f) . (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3)) = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) ) & ( (def_func' H,f) . (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3)) = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) implies E,(f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4)) |= H ) & ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3) = (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . (x. 3) ) by A53, A55, A64, Def1;
then A67: E,(f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4)) |= All (x. 1),(x. 2),H by A54, A60, A61, A63, A64, Th11;
set k = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1));
A68: ( (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . (x. 1) = (i +* (x. 3),a) . (x. 1) & ( for x being Variable st x <> x. 1 holds
(((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . x = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x ) ) by FUNCT_7:34, FUNCT_7:130;
( All (x. 1),(x. 2),H = All (x. 1),(All (x. 2),H) & ( for x being Variable st (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . x <> ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x holds
x. 1 = x ) ) by A68;
then A69: E,((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1)) |= All (x. 2),H by A67, ZF_MODEL:16;

now

let x be Variable; :: thesis:
assume that
A70: (i +* (x. 3),a) . x <> (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . x and
A71: x. 2 <> x ; :: thesis:
A72: x. 1 <> x by A68, A70;
( (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . (x. 3) = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3) & ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3) = (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . (x. 3) ) by A64, A68;
then A73: x. 3 <> x by A63, A70;
( (i +* (x. 3),a) . (x. 4) = i . (x. 4) & (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . (x. 4) = ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) ) by A61, A68;
then A74: x. 4 <> x by A64, A70;
(i +* (x. 3),a) . x = i . x by A61, A73
.= (g +* (x. 2),v) . x by A58, A74
.= g . x by A57, A71
.= f . x by A56, A72
.= (f +* (x. 3),((i +* (x. 3),a) . (x. 3))) . x by A63, A73
.= ((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) . x by A64, A74
.= (((f +* (x. 3),((i +* (x. 3),a) . (x. 3))) +* (x. 4),(i . (x. 4))) +* (x. 1),((i +* (x. 3),a) . (x. 1))) . x by A68, A72 ;
hence contradiction by A70; :: thesis:

end;

then E,i +* (x. 3),a |= H by A69, ZF_MODEL:16;
then ( E,i +* (x. 3),a |= ((x. 3) 'in' (x. 1)) '&' H & ( for x being Variable st (i +* (x. 3),a) . x <> i . x holds
x. 3 = x ) ) by A61, A62, ZF_MODEL:15;
hence E,i |= Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H) by ZF_MODEL:20; :: thesis:

end;

now

assume E,i |= Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H) ; :: thesis:
then consider j being Function of VAR ,E such that
A75: ( ( for x being Variable st j . x <> i . x holds
x. 3 = x ) & E,j |= ((x. 3) 'in' (x. 1)) '&' H ) by ZF_MODEL:20;
A76: ( E,j |= (x. 3) 'in' (x. 1) & E,j |= H ) by A75, ZF_MODEL:15;
then A77: E,j |= All (x. 1),(x. 2),H by A54, Th11;
set m1 = f +* (x. 3),(j . (x. 3));
A78: ( (f +* (x. 3),(j . (x. 3))) . (x. 3) = j . (x. 3) & ( for x being Variable st x <> x. 3 holds
(f +* (x. 3),(j . (x. 3))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
set m = (f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4));
A79: ( ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) = i . (x. 4) & ( for x being Variable st x <> x. 4 holds
((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . x = (f +* (x. 3),(j . (x. 3))) . x ) ) by FUNCT_7:34, FUNCT_7:130;
set k = j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1));
A80: ( (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . (x. 1) = ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1) & ( for x being Variable st x <> x. 1 holds
(j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . x = j . x ) ) by FUNCT_7:34, FUNCT_7:130;
( All (x. 1),(x. 2),H = All (x. 1),(All (x. 2),H) & ( for x being Variable st (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . x <> j . x holds
x. 1 = x ) ) by A80;
then A81: E,j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1)) |= All (x. 2),H by A77, ZF_MODEL:16;

now

let x be Variable; :: thesis:
assume that
A82: ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . x <> (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . x and
A83: x. 2 <> x ; :: thesis:
A84: x. 1 <> x by A80, A82;
( ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3) = (f +* (x. 3),(j . (x. 3))) . (x. 3) & (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . (x. 3) = j . (x. 3) ) by A79, A80;
then A85: x. 3 <> x by A78, A82;
( (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . (x. 4) = j . (x. 4) & j . (x. 4) = i . (x. 4) ) by A75, A80;
then A86: x. 4 <> x by A79, A82;
then ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . x = (f +* (x. 3),(j . (x. 3))) . x by A79
.= f . x by A78, A85
.= g . x by A56, A84
.= (g +* (x. 2),v) . x by A57, A83
.= i . x by A58, A86
.= j . x by A75, A85
.= (j +* (x. 1),(((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 1))) . x by A80, A84 ;
hence contradiction by A82; :: thesis:

end;

then A87: E,(f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4)) |= H by A81, ZF_MODEL:16;

now

let x be Variable; :: thesis:
assume that
A88: ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . x <> f . x and
A89: ( x. 0 <> x & x. 3 <> x & x. 4 <> x ) ; :: thesis:
f . x = (f +* (x. 3),(j . (x. 3))) . x by A78, A89
.= ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . x by A79, A89 ;
hence contradiction by A88; :: thesis:

end;

then A90: ( (def_func' H,f) . (((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3)) = ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 4) & ((f +* (x. 3),(j . (x. 3))) +* (x. 4),(i . (x. 4))) . (x. 3) = (f +* (x. 3),(j . (x. 3))) . (x. 3) ) by A53, A55, A79, A87, Def1;
A91: ( j . (x. 3) in j . (x. 1) & j . (x. 1) = i . (x. 1) & i . (x. 1) = (g +* (x. 2),v) . (x. 1) & (g +* (x. 2),v) . (x. 1) = g . (x. 1) ) by A57, A58, A75, A76, ZF_MODEL:13;
( j . (x. 3) in E & dom (def_func' H,f) = E ) by FUNCT_2:def 1;
then A92: i . (x. 4) in (def_func' H,f) .: (g . (x. 1)) by A78, A79, A90, A91, FUNCT_1:def 12;
i . (x. 2) = (g +* (x. 2),v) . (x. 2) by A58;
hence E,i |= (x. 4) 'in' (x. 2) by A57, A92, ZF_MODEL:13; :: thesis:

end;

hence E,i |= ((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A59, ZF_MODEL:19; :: thesis:

end;

then ( E,g +* (x. 2),v |= All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))) & ( for x being Variable st (g +* (x. 2),v) . x <> g . x holds
x. 2 = x ) ) by A57, ZF_MODEL:16;
hence E,g |= Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)))) by ZF_MODEL:20; :: thesis:

end;

hence E,f |= All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))))) by ZF_MODEL:16; :: thesis:

end;

hence E,f |= the_axiom_of_substitution_for H by ZF_MODEL:18; :: thesis:

end;

hence ( ( for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR ,E st {(x. 0 ),(x. 1),(x. 2)} misses Free H & E,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for u being Element of E holds (def_func' H,f) .: u in E ) by A2; :: thesis: