let W be Universe; :: thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H
let L be DOMAIN-Sequence of W; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H )
assume that
A1: omega in W and
A2: for a, b being Ordinal of W st a in b holds
L . a c= L . b and
A3: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) and
A4: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A5: Union L is predicatively_closed ; :: thesis: for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H
set M = Union L;

A6: now

defpred S₁[ set , set ] means $1 in L . $2;
let H be ZF-formula; :: thesis: for f being Function of VAR ,(Union L) st {(x. 0 ),(x. 1),(x. 2)} misses Free H & Union L,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for u being Element of Union L holds (def_func' H,f) .: u in Union L
let f be Function of VAR ,(Union L); :: thesis: ( {(x. 0 ),(x. 1),(x. 2)} misses Free H & Union L,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) implies for u being Element of Union L holds (def_func' H,f) .: u in Union L )
assume that
A7: {(x. 0 ),(x. 1),(x. 2)} misses Free H and
A8: Union L,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis: for u being Element of Union L holds (def_func' H,f) .: u in Union L
consider k being Element of NAT such that
A9: for i being Element of NAT st x. i in variables_in H holds
i < k by ZFMODEL2:4;
set p = H / (x. 0 ),(x. (k + 5));
k + 0 = k ;
then A10: not x. (k + 5) in variables_in H by A9, XREAL_1:9;
then A11: ( Union L,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),((H / (x. 0 ),(x. (k + 5))) <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,f = def_func' (H / (x. 0 ),(x. (k + 5))),f ) by A7, A8, Lm2;
set F = def_func' H,f;
A12: for d being Element of Union L ex a being Ordinal of W st S₁[d,a]

proof

let d be Element of Union L; :: thesis: ex a being Ordinal of W st S₁[d,a]
consider u being set such that
A13: u in dom L and
A14: d in L . u by Lm1;
u in On W by A13, ZF_REFLE:def 5;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
take u ; :: thesis: S₁[d,u]
thus S₁[d,u] by A14; :: thesis: verum

end;

consider g being Function such that
A15: ( dom g = Union L & ( for d being Element of Union L ex a being Ordinal of W st
( a = g . d & S₁[d,a] & ( for b being Ordinal of W st S₁[d,b] holds
a c= b ) ) ) ) from ZF_REFLE:sch 1(A12);
A16: rng g c= W

proof

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in rng g or u1 in W )
assume u1 in rng g ; :: thesis: u1 in W
then consider u2 being set such that
A17: u2 in dom g and
A18: u1 = g . u2 by FUNCT_1:def 5;
reconsider d = u2 as Element of Union L by A15, A17;
ex a being Ordinal of W st
( a = g . d & d in L . a & ( for b being Ordinal of W st d in L . b holds
a c= b ) ) by A15;
hence u1 in W by A18; :: thesis: verum

end;

( card VAR = omega & omega in card W ) by A1, CARD_1:21, CARD_1:84, CLASSES2:1, ZF_REFLE:25;
then A19: card (dom f) in card W by FUNCT_2:def 1;
rng f = f .: (dom f) by RELAT_1:146;
then card (rng f) in card W by A19, CARD_2:3, ORDINAL1:22;
then A20: card (g .: (rng f)) in card W by CARD_2:3, ORDINAL1:22;
g .: (rng f) c= rng g by RELAT_1:144;
then g .: (rng f) c= W by A16, XBOOLE_1:1;
then g .: (rng f) in W by A20, CLASSES1:2;
then reconsider b2 = sup (g .: (rng f)) as Ordinal of W by ZF_REFLE:28;
A21: x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
{(x. 0 ),(x. 1),(x. 2)} misses Free (H / (x. 0 ),(x. (k + 5))) by A7, A8, A10, Lm2;
then A22: not x. 0 in Free (H / (x. 0 ),(x. (k + 5))) by A21, XBOOLE_0:3;
A23: for X being set
for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds
X c= L . a

proof

let X be set ; :: thesis: for a being Ordinal of W st X c= Union L & sup (g .: X) c= a holds
X c= L . a
let a be Ordinal of W; :: thesis: ( X c= Union L & sup (g .: X) c= a implies X c= L . a )
assume that
A24: X c= Union L and
A25: sup (g .: X) c= a ; :: thesis: X c= L . a
let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in L . a )
assume A26: u1 in X ; :: thesis: u1 in L . a
then reconsider d = u1 as Element of Union L by A24;
consider b being Ordinal of W such that
A27: b = g . d and
A28: d in L . b and
for a being Ordinal of W st d in L . a holds
b c= a by A15;
b in g .: X by A15, A26, A27, FUNCT_1:def 12;
then b in sup (g .: X) by ORDINAL2:27;
then L . b c= L . a by A2, A25;
hence u1 in L . a by A28; :: thesis: verum

end;

let u be Element of Union L; :: thesis: (def_func' H,f) .: u in Union L
consider b0 being Ordinal of W such that
b0 = g . u and
A29: u in L . b0 and
for b being Ordinal of W st u in L . b holds
b0 c= b by A15;
A30: card u in card W by CLASSES2:1;
k + 0 = k ;
then A31: ( 0 <= k & k < k + 5 ) by NAT_1:2, XREAL_1:8;
then A32: not x. 0 in variables_in (H / (x. 0 ),(x. (k + 5))) by ZF_LANG1:86, ZF_LANG1:198;
g .: ((def_func' H,f) .: u) c= rng g by RELAT_1:144;
then A33: g .: ((def_func' H,f) .: u) c= W by A16, XBOOLE_1:1;
( card (g .: ((def_func' H,f) .: u)) c= card ((def_func' H,f) .: u) & card ((def_func' H,f) .: u) c= card u ) by CARD_2:3;
then card (g .: ((def_func' H,f) .: u)) in card W by A30, ORDINAL1:22, XBOOLE_1:1;
then g .: ((def_func' H,f) .: u) in W by A33, CLASSES1:2;
then reconsider b1 = sup (g .: ((def_func' H,f) .: u)) as Ordinal of W by ZF_REFLE:28;
set b = b0 \/ b1;
set a = (b0 \/ b1) \/ b2;
A34: (def_func' H,f) .: u c= L . (b0 \/ b1) by A23, XBOOLE_1:7;
consider phi being Ordinal-Sequence of W such that
A35: ( phi is increasing & phi is continuous ) and
A36: for a being Ordinal of W st phi . a = a & {} <> a holds
for v being Function of VAR ,(L . a) holds
( Union L,(Union L) ! v |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) iff L . a,v |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) ) by A1, A2, A3, ZF_REFLE:29;
consider a1 being Ordinal of W such that
A37: (b0 \/ b1) \/ b2 in a1 and
A38: phi . a1 = a1 by A1, A35, ZFREFLE1:30;
A39: rng f c= L . a1

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in L . a1 )
A40: b2 c= (b0 \/ b1) \/ b2 by XBOOLE_1:7;
assume A41: u in rng f ; :: thesis: u in L . a1
then consider u1 being set such that
A42: u1 in dom f and
A43: u = f . u1 by FUNCT_1:def 5;
reconsider u1 = u1 as Variable by A42;
consider a2 being Ordinal of W such that
A44: a2 = g . (f . u1) and
A45: f . u1 in L . a2 and
for b being Ordinal of W st f . u1 in L . b holds
a2 c= b by A15;
a2 in g .: (rng f) by A15, A41, A43, A44, FUNCT_1:def 12;
then a2 in b2 by ORDINAL2:27;
then L . a2 c= L . a1 by A2, A37, A40, ORDINAL1:19;
hence u in L . a1 by A43, A45; :: thesis: verum

end;

set x = x. (k + 10);
k + 0 = k ;
then not k + 10 < k by XREAL_1:8;
then not x. (k + 10) in variables_in H by A9;
then A46: not x. (k + 10) in (variables_in H) \ {(x. 0 )} by XBOOLE_0:def 5;
set q = Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )));
A47: 10 <= 10 + k by NAT_1:11;
( b0 c= b0 \/ b1 & b0 \/ b1 c= (b0 \/ b1) \/ b2 ) by XBOOLE_1:7;
then b0 c= (b0 \/ b1) \/ b2 by XBOOLE_1:1;
then A48: L . b0 c= L . a1 by A2, A37, ORDINAL1:22;
then reconsider mu = u as Element of L . a1 by A29;
dom f = VAR by FUNCT_2:def 1;
then reconsider v = f as Function of VAR ,(L . a1) by A39, FUNCT_2:def 1, RELSET_1:11;
set w = (v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu;
A49: ( x. (k + 10) <> x. (k + 5) implies not x. (k + 10) in {(x. (k + 5))} ) by TARSKI:def 1;
( variables_in (H / (x. 0 ),(x. (k + 5))) c= ((variables_in H) \ {(x. 0 )}) \/ {(x. (k + 5))} & k + 5 <> k + 10 ) by ZF_LANG1:201;
then not x. (k + 10) in variables_in (H / (x. 0 ),(x. (k + 5))) by A46, A49, XBOOLE_0:def 3, ZF_LANG1:86;
then A50: ( variables_in ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) c= ((variables_in (H / (x. 0 ),(x. (k + 5)))) \ {(x. 4)}) \/ {(x. 0 )} & not x. (k + 10) in (variables_in (H / (x. 0 ),(x. (k + 5)))) \ {(x. 4)} ) by XBOOLE_0:def 5, ZF_LANG1:201;
A51: 10 > 0 ;
then A52: x. (k + 10) <> x. 0 by A47, ZF_LANG1:86;
then not x. (k + 10) in {(x. 0 )} by TARSKI:def 1;
then A53: not x. (k + 10) in variables_in ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) by A50, XBOOLE_0:def 3;
A54: 10 > 3 ;
then A55: ( x. 0 <> x. 3 & x. (k + 10) <> x. 3 ) by A47, ZF_LANG1:86;
b0 \/ b1 in a1 by A37, ORDINAL1:22, XBOOLE_1:7;
then L . (b0 \/ b1) c= L . a1 by A2;
then A56: (def_func' H,f) .: u c= L . a1 by A34, XBOOLE_1:1;
A57: (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu)

proof

now

per cases ( x. 4 in Free H or not x. 4 in Free H ) ;

suppose A58: x. 4 in Free H ; :: thesis: (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu)

4 <> k + 5 by NAT_1:11;
then A59: x. (k + 5) <> x. 4 by ZF_LANG1:86;
A60: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:86;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:86;
then A61: x. 0 in Free (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))) by A58, A60, A59, Lm4;
A62: (def_func' H,f) .: u c= Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu)

proof

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in (def_func' H,f) .: u or u1 in Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) )
assume A63: u1 in (def_func' H,f) .: u ; :: thesis: u1 in Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu)
then consider u2 being set such that
A64: u2 in dom (def_func' H,f) and
A65: u2 in u and
A66: u1 = (def_func' H,f) . u2 by FUNCT_1:def 12;
reconsider m1 = u1 as Element of L . a1 by A56, A63;
reconsider u2 = u2 as Element of Union L by A64;
L . a1 is epsilon-transitive by A4;
then u c= L . a1 by A29, A48, ORDINAL1:def 2;
then reconsider m2 = u2 as Element of L . a1 by A65;
A67: (f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2) = (Union L) ! ((v / (x. 3),m2) / (x. 0 ),m1) by A66, ZF_LANG1:def 2, ZF_REFLE:24;
( Union L,(f / (x. 3),u2) / (x. 4),((def_func' H,f) . u2) |= H / (x. 0 ),(x. (k + 5)) & ((f / (x. 3),u2) / (x. 4),((def_func' H,f) . u2)) . (x. 4) = (def_func' H,f) . u2 ) by A11, A22, FUNCT_7:130, ZFMODEL2:11;
then Union L,((f / (x. 3),u2) / (x. 4),((def_func' H,f) . u2)) / (x. 0 ),((def_func' H,f) . u2) |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A32, ZFMODEL2:14;
then A68: Union L,((f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2)) / (x. 4),((def_func' H,f) . u2) |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by FUNCT_7:35, ZF_LANG1:86;
not x. 4 in variables_in ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) by ZF_LANG1:86, ZF_LANG1:198;
then Union L,(f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2) |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A68, ZFMODEL2:6;
then L . a1,(v / (x. 3),m2) / (x. 0 ),m1 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A36, A37, A38, A67;
then A69: L . a1,((v / (x. 3),m2) / (x. 0 ),m1) / (x. (k + 10)),mu |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A53, ZFMODEL2:6;
A70: ( ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) . (x. (k + 10)) = (((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) . (x. (k + 10)) & ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:34, FUNCT_7:130, ZF_LANG1:86;
( ((((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2) . (x. 3) = m2 & ((((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2) . (x. (k + 10)) = (((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) . (x. (k + 10)) ) by A54, A47, FUNCT_7:34, FUNCT_7:130, ZF_LANG1:86;
then A71: L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= (x. 3) 'in' (x. (k + 10)) by A65, A70, ZF_MODEL:13;
((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1 = (v / (x. (k + 10)),mu) / (x. 0 ),m1 by ZFMODEL2:9;
then L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A52, A55, A69, ZFMODEL2:7;
then L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) by A71, ZF_MODEL:15;
then L . a1,((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1 |= Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ))) by ZF_LANG1:82;
then u1 in { m where m is Element of L . a1 : L . a1,((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m |= Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ))) } ;
hence u1 in Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) by A61, Def1; :: thesis: verum

end;

Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) c= (def_func' H,f) .: u

proof

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) or u1 in (def_func' H,f) .: u )
A72: L . a1 c= Union L by ZF_REFLE:24;
assume u1 in Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) ; :: thesis: u1 in (def_func' H,f) .: u
then u1 in { m where m is Element of L . a1 : L . a1,((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m |= Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ))) } by A61, Def1;
then consider m1 being Element of L . a1 such that
A73: u1 = m1 and
A74: L . a1,((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1 |= Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ))) ;
consider m2 being Element of L . a1 such that
A75: L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= ((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) by A74, ZF_LANG1:82;
( m1 in L . a1 & m2 in L . a1 ) ;
then reconsider u9 = m1, u2 = m2 as Element of Union L by A72;
A76: ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1 = (v / (x. (k + 10)),mu) / (x. 0 ),m1 by ZFMODEL2:9;
L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A75, ZF_MODEL:15;
then L . a1,((v / (x. 3),m2) / (x. 0 ),m1) / (x. (k + 10)),mu |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A52, A55, A76, ZFMODEL2:7;
then A77: L . a1,(v / (x. 3),m2) / (x. 0 ),m1 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A53, ZFMODEL2:6;
A78: ( ((f / (x. 3),u2) / (x. 0 ),u9) / (x. 4),u9 = ((f / (x. 3),u2) / (x. 4),u9) / (x. 0 ),u9 & ((f / (x. 3),u2) / (x. 0 ),u9) . (x. 0 ) = u9 ) by FUNCT_7:35, FUNCT_7:130, ZF_LANG1:86;
(f / (x. 3),u2) / (x. 0 ),u9 = (Union L) ! ((v / (x. 3),m2) / (x. 0 ),m1) by ZF_LANG1:def 2, ZF_REFLE:24;
then Union L,(f / (x. 3),u2) / (x. 0 ),u9 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A36, A37, A38, A77;
then Union L,((f / (x. 3),u2) / (x. 4),u9) / (x. 0 ),u9 |= H / (x. 0 ),(x. (k + 5)) by A32, A78, ZFMODEL2:13;
then Union L,(f / (x. 3),u2) / (x. 4),u9 |= H / (x. 0 ),(x. (k + 5)) by A32, ZFMODEL2:6;
then A79: (def_func' H,f) . u2 = u9 by A11, A22, ZFMODEL2:11;
A80: ( ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) . (x. (k + 10)) = (((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) . (x. (k + 10)) & ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) . (x. (k + 10)) = mu ) by A51, A47, FUNCT_7:34, FUNCT_7:130, ZF_LANG1:86;
A81: L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= (x. 3) 'in' (x. (k + 10)) by A75, ZF_MODEL:15;
A82: dom (def_func' H,f) = Union L by FUNCT_2:def 1;
( ((((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2) . (x. 3) = m2 & ((((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2) . (x. (k + 10)) = (((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) . (x. (k + 10)) ) by A54, A47, FUNCT_7:34, FUNCT_7:130, ZF_LANG1:86;
then m2 in u by A81, A80, ZF_MODEL:13;
hence u1 in (def_func' H,f) .: u by A73, A79, A82, FUNCT_1:def 12; :: thesis: verum

end;

hence (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) by A62, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A83: not x. 4 in Free H ; :: thesis: (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu)

4 <> k + 5 by NAT_1:11;
then A84: x. (k + 5) <> x. 4 by ZF_LANG1:86;
A85: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:86;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:86;
then not x. 0 in Free (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))) by A83, A85, A84, Lm4;
then Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) = {} by Def1;
hence (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) by A8, A83, Lm3; :: thesis: verum

end;

end;

end;

hence (def_func' H,f) .: u = Section (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))),((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) ; :: thesis: verum

end;

L . a1 in Union L by A4;
hence (def_func' H,f) .: u in Union L by A5, A57, Def2; :: thesis: verum

end;

Union L is epsilon-transitive

proof

let X be set ; :: according to ORDINAL1:def 2 :: thesis: ( not X in Union L or X c= Union L )
assume X in Union L ; :: thesis: X c= Union L
then consider u being set such that
A86: u in dom L and
A87: X in L . u by Lm1;
reconsider u = u as Ordinal by A86;
u in On W by A86, ZF_REFLE:def 5;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
L . u is epsilon-transitive by A4;
then A88: X c= L . u by A87, ORDINAL1:def 2;
let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in Union L )
A89: L . u c= Union L by ZF_REFLE:24;
assume u1 in X ; :: thesis: u1 in Union L
then u1 in L . u by A88;
hence u1 in Union L by A89; :: thesis: verum

end;

hence for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H by A6, ZFMODEL1:19; :: thesis: verum