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 :: thesis:

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:
E |= the_axiom_of_substitution_for H by A3, A4;
then E,f |= the_axiom_of_substitution_for H ;
then A6: 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;
let u be Element of E; :: thesis:
set g = f +* ((x. 1),u);
x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A7: not x. 0 in Free H by A4, XBOOLE_0:3;

now :: thesis:

let a be object ; :: 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 A8: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
for x being Variable st (f +* ((x. 1),u)) . x <> f . x holds
x. 1 = x by FUNCT_7:32;
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 A6, ZF_MODEL:16;
then consider h being Function of VAR,E such that
A9: for x being Variable st h . x <> (f +* ((x. 1),u)) . x holds
x. 2 = x and
A10: 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: (f +* ((x. 1),u)) . (x. 1) = u by FUNCT_7:128;
A12: (def_func' (H,f)) .: u c= h . (x. 2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: a in (def_func' (H,f)) .: u ; :: thesis:
then consider b being object such that
A14: b in dom (def_func' (H,f)) and
A15: b in u and
A16: (def_func' (H,f)) . b = a by FUNCT_1:def 6;
reconsider b = b as Element of E by A14;
reconsider e = a as Element of E by A13;
set i = h +* ((x. 4),e);
set j = (h +* ((x. 4),e)) +* ((x. 3),b);
A17: ((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
A18: h . (x. 1) = (f +* ((x. 1),u)) . (x. 1) by A9;
( ((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1) = (h +* ((x. 4),e)) . (x. 1) & (h +* ((x. 4),e)) . (x. 1) = h . (x. 1) ) by FUNCT_7:32;
then A19: E,(h +* ((x. 4),e)) +* ((x. 3),b) |= (x. 3) 'in' (x. 1) by A11, A15, A17, A18, ZF_MODEL:13;
set m1 = f +* ((x. 3),b);
A20: (h +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
set m = (f +* ((x. 3),b)) +* ((x. 4),e);
A21: (f +* ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
set k = ((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)));
A22: ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
A23: ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 3) = (f +* ((x. 3),b)) . (x. 3) by FUNCT_7:32;

A24: now :: thesis:

let x be Variable; :: thesis:
assume that
A25: ((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
A26: x. 2 <> x ; :: thesis:
A27: x <> x. 3 by A17, A21, A23, A25, FUNCT_7:32;
(((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) by FUNCT_7:32;
then A28: x <> x. 4 by A20, A22, A25, FUNCT_7:32;
A29: x <> x. 1 by A25, FUNCT_7:128;
then (((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:32
.= (f +* ((x. 3),b)) . x by A28, FUNCT_7:32
.= f . x by A27, FUNCT_7:32
.= (f +* ((x. 1),u)) . x by A29, FUNCT_7:32
.= h . x by A9, A26
.= (h +* ((x. 4),e)) . x by A28, FUNCT_7:32
.= ((h +* ((x. 4),e)) +* ((x. 3),b)) . x by A27, FUNCT_7:32 ;
hence contradiction by A25; :: thesis:

end;

A30: 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 FUNCT_7:32;

now :: thesis:

let y be Variable; :: thesis:
assume A31: ((f +* ((x. 3),b)) +* ((x. 4),e)) . y <> f . y ; :: thesis:
assume that
x. 0 <> y and
A32: x. 3 <> y and
A33: x. 4 <> y ; :: thesis:
((f +* ((x. 3),b)) +* ((x. 4),e)) . y = (f +* ((x. 3),b)) . y by A33, FUNCT_7:32;
hence contradiction by A31, A32, FUNCT_7:32; :: thesis:

end;

then ( 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, A7, Def1;
then E,(f +* ((x. 3),b)) +* ((x. 4),e) |= All ((x. 1),(x. 2),H) by A8, A16, A21, A22, Th11, FUNCT_7:32;
then E,((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1))) |= All ((x. 2),H) by A30, ZF_MODEL:16;
then E,(h +* ((x. 4),e)) +* ((x. 3),b) |= H by A24, ZF_MODEL:16;
then A34: E,(h +* ((x. 4),e)) +* ((x. 3),b) |= ((x. 3) 'in' (x. 1)) '&' H by A19, ZF_MODEL:15;
for x being Variable st (h +* ((x. 4),e)) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then A35: E,h +* ((x. 4),e) |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))) by A10, ZF_MODEL:16;
A36: (h +* ((x. 4),e)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
for x being Variable st (h +* ((x. 4),e)) . x <> ((h +* ((x. 4),e)) +* ((x. 3),b)) . x holds
x. 3 = x by FUNCT_7:32;
then E,h +* ((x. 4),e) |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A34, ZF_MODEL:20;
then E,h +* ((x. 4),e) |= (x. 4) 'in' (x. 2) by A35, ZF_MODEL:19;
hence a in h . (x. 2) by A20, A36, ZF_MODEL:13; :: thesis:

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A37: a in h . (x. 2) ; :: thesis:
h . (x. 2) c= E by A1;
then reconsider e = a as Element of E by A37;
set i = h +* ((x. 4),e);
A38: (h +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
for x being Variable st (h +* ((x. 4),e)) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then A39: 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 FUNCT_7:32;
then E,h +* ((x. 4),e) |= (x. 4) 'in' (x. 2) by A37, A38, ZF_MODEL:13;
then E,h +* ((x. 4),e) |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A39, ZF_MODEL:19;
then consider j being Function of VAR,E such that
A40: for x being Variable st j . x <> (h +* ((x. 4),e)) . x holds
x. 3 = x and
A41: E,j |= ((x. 3) 'in' (x. 1)) '&' H by ZF_MODEL:20;
A42: j . (x. 1) = (h +* ((x. 4),e)) . (x. 1) by A40;
set m1 = f +* ((x. 3),(j . (x. 3)));
set m = (f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e);
A43: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
set k = j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)));
A44: (f +* ((x. 3),(j . (x. 3)))) . (x. 3) = j . (x. 3) by FUNCT_7:128;

A45: now :: thesis:

let x be Variable; :: thesis:
assume that
A46: ((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
A47: x. 2 <> x ; :: thesis:
(j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . (x. 3) = j . (x. 3) by FUNCT_7:32;
then A48: x. 3 <> x by A44, A46, FUNCT_7:32;
(j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . (x. 4) = j . (x. 4) by FUNCT_7:32;
then A49: x. 4 <> x by A38, A40, A43, A46;
A50: x. 1 <> x by A46, FUNCT_7:128;
then (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . x = j . x by FUNCT_7:32
.= (h +* ((x. 4),e)) . x by A40, A48
.= h . x by A49, FUNCT_7:32
.= (f +* ((x. 1),u)) . x by A9, A47
.= f . x by A50, FUNCT_7:32
.= (f +* ((x. 3),(j . (x. 3)))) . x by A48, FUNCT_7:32
.= ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . x by A49, FUNCT_7:32 ;
hence contradiction by A46; :: thesis:

end;

now :: thesis:

let y be Variable; :: thesis:
assume A51: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . y <> f . y ; :: thesis:
assume that
x. 0 <> y and
A52: x. 3 <> y and
A53: x. 4 <> y ; :: thesis:
((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . y = (f +* ((x. 3),(j . (x. 3)))) . y by A53, FUNCT_7:32;
hence contradiction by A51, A52, FUNCT_7:32; :: thesis:

end;

then A54: ( 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, A7, Def1;
E,j |= (x. 3) 'in' (x. 1) by A41, ZF_MODEL:15;
then A55: j . (x. 3) in j . (x. 1) by ZF_MODEL:13;
E,j |= H by A41, ZF_MODEL:15;
then A56: E,j |= All ((x. 1),(x. 2),H) by A8, Th11;
A57: ( (h +* ((x. 4),e)) . (x. 1) = h . (x. 1) & h . (x. 1) = (f +* ((x. 1),u)) . (x. 1) ) by A9, FUNCT_7:32;
A58: dom (def_func' (H,f)) = E by FUNCT_2:def 1;
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 FUNCT_7:32;
then E,j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1))) |= All ((x. 2),H) by A56, ZF_MODEL:16;
then (def_func' (H,f)) . (j . (x. 3)) = a by A44, A43, A54, A45, FUNCT_7:32, ZF_MODEL:16;
hence a in (def_func' (H,f)) .: u by A11, A55, A42, A57, A58, FUNCT_1:def 6; :: thesis:

end;

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

end;

now :: thesis:

assume A59: 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 A60: {(x. 0),(x. 1),(x. 2)} misses Free H ; :: thesis:

now :: thesis:

let a be object ; :: 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 A60, XBOOLE_0:3; :: thesis:

end;

then A61: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A62: not x. 0 in Free H by A60, 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 :: thesis:

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

now :: thesis:

let g be Function of VAR,E; :: thesis:
assume A64: 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 A59, A60, A63;
set h = g +* ((x. 2),v);
A65: (g +* ((x. 2),v)) . (x. 2) = v by FUNCT_7:128;

now :: thesis:

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

A67: now :: thesis:

assume E,i |= (x. 4) 'in' (x. 2) ; :: thesis:
then A68: i . (x. 4) in i . (x. 2) by ZF_MODEL:13;
i . (x. 2) = (g +* ((x. 2),v)) . (x. 2) by A66;
then consider a being object such that
A69: a in dom (def_func' (H,f)) and
A70: a in g . (x. 1) and
A71: i . (x. 4) = (def_func' (H,f)) . a by A65, A68, FUNCT_1:def 6;
reconsider a = a as Element of E by A69;
set j = i +* ((x. 3),a);
A72: (i +* ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
set m1 = f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)));
set m = (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)));
A73: ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) = i . (x. 4) by FUNCT_7:128;
set k = ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)));
A74: (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) . (x. 3) = (i +* ((x. 3),a)) . (x. 3) by FUNCT_7:128;

A75: now :: thesis:

let x be Variable; :: thesis:
assume that
A76: (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
A77: x. 2 <> x ; :: thesis:
A78: x. 1 <> x by A76, FUNCT_7:128;
(i +* ((x. 3),a)) . (x. 4) = i . (x. 4) by FUNCT_7:32;
then A79: x. 4 <> x by A73, A76, FUNCT_7:32;
(((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) by FUNCT_7:32;
then A80: x. 3 <> x by A74, A76, FUNCT_7:32;
then (i +* ((x. 3),a)) . x = i . x by FUNCT_7:32
.= (g +* ((x. 2),v)) . x by A66, A79
.= g . x by A77, FUNCT_7:32
.= f . x by A64, A78
.= (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) . x by A80, FUNCT_7:32
.= ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x by A79, FUNCT_7:32
.= (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . x by A78, FUNCT_7:32 ;
hence contradiction by A76; :: thesis:

end;

A81: 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 FUNCT_7:32;

now :: thesis:

let x be Variable; :: thesis:
assume that
A82: ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x and
x. 0 <> x and
A83: x. 3 <> x and
A84: 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 by A84, FUNCT_7:32;
hence contradiction by A82, A83, FUNCT_7:32; :: thesis:

end;

then ( E,(f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= H iff (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) ) by A62, A63, Def1;
then E,(f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= All ((x. 1),(x. 2),H) by A61, A71, A72, A74, A73, Th11, FUNCT_7:32;
then 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 A81, ZF_MODEL:16;
then A85: E,i +* ((x. 3),a) |= H by A75, ZF_MODEL:16;
A86: (g +* ((x. 2),v)) . (x. 1) = g . (x. 1) by FUNCT_7:32;
( (i +* ((x. 3),a)) . (x. 1) = i . (x. 1) & i . (x. 1) = (g +* ((x. 2),v)) . (x. 1) ) by A66, FUNCT_7:32;
then E,i +* ((x. 3),a) |= (x. 3) 'in' (x. 1) by A70, A72, A86, ZF_MODEL:13;
then A87: E,i +* ((x. 3),a) |= ((x. 3) 'in' (x. 1)) '&' H by A85, ZF_MODEL:15;
for x being Variable st (i +* ((x. 3),a)) . x <> i . x holds
x. 3 = x by FUNCT_7:32;
hence E,i |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A87, ZF_MODEL:20; :: thesis:

end;

now :: thesis:

assume E,i |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) ; :: thesis:
then consider j being Function of VAR,E such that
A88: for x being Variable st j . x <> i . x holds
x. 3 = x and
A89: E,j |= ((x. 3) 'in' (x. 1)) '&' H by ZF_MODEL:20;
set m1 = f +* ((x. 3),(j . (x. 3)));
set m = (f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)));
A90: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) = i . (x. 4) by FUNCT_7:128;
set k = j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)));
A91: (f +* ((x. 3),(j . (x. 3)))) . (x. 3) = j . (x. 3) by FUNCT_7:128;

A92: now :: thesis:

let x be Variable; :: thesis:
assume that
A93: ((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
A94: x. 2 <> x ; :: thesis:
A95: x. 1 <> x by A93, FUNCT_7:128;
((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3) = (f +* ((x. 3),(j . (x. 3)))) . (x. 3) by FUNCT_7:32;
then A96: x. 3 <> x by A91, A93, FUNCT_7:32;
(j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . (x. 4) = j . (x. 4) by FUNCT_7:32;
then A97: x. 4 <> x by A88, A90, A93;
then ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x = (f +* ((x. 3),(j . (x. 3)))) . x by FUNCT_7:32
.= f . x by A96, FUNCT_7:32
.= g . x by A64, A95
.= (g +* ((x. 2),v)) . x by A94, FUNCT_7:32
.= i . x by A66, A97
.= j . x by A88, A96
.= (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . x by A95, FUNCT_7:32 ;
hence contradiction by A93; :: thesis:

end;

A98: i . (x. 2) = (g +* ((x. 2),v)) . (x. 2) by A66;
A99: ( (g +* ((x. 2),v)) . (x. 1) = g . (x. 1) & dom (def_func' (H,f)) = E ) by FUNCT_2:def 1, FUNCT_7:32;
E,j |= (x. 3) 'in' (x. 1) by A89, ZF_MODEL:15;
then A100: j . (x. 3) in j . (x. 1) by ZF_MODEL:13;

A101: now :: thesis:

let x be Variable; :: thesis:
assume that
A102: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x and
x. 0 <> x and
A103: x. 3 <> x and
A104: x. 4 <> x ; :: thesis:
f . x = (f +* ((x. 3),(j . (x. 3)))) . x by A103, FUNCT_7:32
.= ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x by A104, FUNCT_7:32 ;
hence contradiction by A102; :: thesis:

end;

E,j |= H by A89, ZF_MODEL:15;
then A105: E,j |= All ((x. 1),(x. 2),H) by A61, Th11;
A106: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3) = (f +* ((x. 3),(j . (x. 3)))) . (x. 3) & i . (x. 1) = (g +* ((x. 2),v)) . (x. 1) ) by A66, FUNCT_7:32;
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 FUNCT_7:32;
then E,j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1))) |= All ((x. 2),H) by A105, ZF_MODEL:16;
then E,(f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= H by A92, ZF_MODEL:16;
then A107: (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) by A62, A63, A101, Def1;
j . (x. 1) = i . (x. 1) by A88;
then i . (x. 4) in (def_func' (H,f)) .: (g . (x. 1)) by A91, A90, A107, A100, A106, A99, FUNCT_1:def 6;
hence E,i |= (x. 4) 'in' (x. 2) by A65, A98, ZF_MODEL:13; :: thesis:

end;

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

end;

then A108: E,g +* ((x. 2),v) |= All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))) by ZF_MODEL:16;
for x being Variable st (g +* ((x. 2),v)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
hence E,g |= Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))) by A108, 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: