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 :: thesis: for H being ZF-formula
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

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:3;
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:7;
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 2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
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 object ; :: 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 object such that
A17: u2 in dom g and
A18: u1 = g . u2 by FUNCT_1:def 3;
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:5, CARD_1:47, CLASSES2:1, ZF_REFLE:17;
then A19: card (dom f) in card W by FUNCT_2:def 1;
rng f = f .: (dom f) by RELAT_1:113;
then card (rng f) in card W by A19, CARD_1:67, ORDINAL1:12;
then A20: card (g .: (rng f)) in card W by CARD_1:67, ORDINAL1:12;
g .: (rng f) c= rng g by RELAT_1:111;
then g .: (rng f) c= W by A16;
then g .: (rng f) in W by A20, CLASSES1:1;
then reconsider b2 = sup (g .: (rng f)) as Ordinal of W by ZF_REFLE:19;
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 object ; :: 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 6;
then b in sup (g .: X) by ORDINAL2:19;
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:6;
then A32: not x. 0 in variables_in (H / ((x. 0),(x. (k + 5)))) by ZF_LANG1:76, ZF_LANG1:184;
g .: ((def_func' (H,f)) .: u) c= rng g by RELAT_1:111;
then A33: g .: ((def_func' (H,f)) .: u) c= W by A16;
( 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_1:67;
then card (g .: ((def_func' (H,f)) .: u)) in card W by A30, ORDINAL1:12, XBOOLE_1:1;
then g .: ((def_func' (H,f)) .: u) in W by A33, CLASSES1:1;
then reconsider b1 = sup (g .: ((def_func' (H,f)) .: u)) as Ordinal of W by ZF_REFLE:19;
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:20;
consider a1 being Ordinal of W such that
A37: (b0 \/ b1) \/ b2 in a1 and
A38: phi . a1 = a1 by A1, A35, ZFREFLE1:28;
A39: rng f c= L . a1

proof

let u be object ; :: 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 object such that
A42: u1 in dom f and
A43: u = f . u1 by FUNCT_1:def 3;
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 6;
then a2 in b2 by ORDINAL2:19;
then L . a2 c= L . a1 by A2, A37, A40, ORDINAL1:10;
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:6;
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 ;
then A48: L . b0 c= L . a1 by A2, A37, ORDINAL1:12;
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:4;
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:187;
then not x. (k + 10) in variables_in (H / ((x. 0),(x. (k + 5)))) by A46, A49, XBOOLE_0:def 3, ZF_LANG1:76;
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:187;
A51: 10 > 0 ;
then A52: x. (k + 10) <> x. 0 by A47, ZF_LANG1:76;
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:76;
b0 \/ b1 in a1 by A37, ORDINAL1:12, XBOOLE_1:7;
then L . (b0 \/ b1) c= L . a1 by A2;
then A56: (def_func' (H,f)) .: u c= L . a1 by A34;
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 :: 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)))

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:76;
A60: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76;
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 object ; :: 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 object 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 6;
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;
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 1, ZF_REFLE:16;
( 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:128, ZFMODEL2:10;
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:13;
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:33, ZF_LANG1:76;
not x. 4 in variables_in ((H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0))) by ZF_LANG1:76, ZF_LANG1:184;
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:5;
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:5;
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:32, FUNCT_7:128, ZF_LANG1:76;
( ((((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:32, FUNCT_7:128, ZF_LANG1:76;
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:8;
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:6;
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:73;
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 object ; :: 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:16;
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:73;
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:8;
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:6;
then A77: L . a1,(v / ((x. 3),m2)) / ((x. 0),m1) |= (H / ((x. 0),(x. (k + 5)))) / ((x. 4),(x. 0)) by A53, ZFMODEL2:5;
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:33, FUNCT_7:128, ZF_LANG1:76;
(f / ((x. 3),u2)) / ((x. 0),u9) = (Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) by ZF_LANG1:def 1, ZF_REFLE:16;
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:12;
then Union L,(f / ((x. 3),u2)) / ((x. 4),u9) |= H / ((x. 0),(x. (k + 5))) by A32, ZFMODEL2:5;
then A79: (def_func' (H,f)) . u2 = u9 by A11, A22, ZFMODEL2:10;
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:32, FUNCT_7:128, ZF_LANG1:76;
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:32, FUNCT_7:128, ZF_LANG1:76;
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 6; :: 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; :: 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:76;
A85: x. (k + 10) <> x. 0 by A51, A47, ZF_LANG1:76;
( not x. (k + 5) in variables_in H & x. (k + 5) <> x. 0 ) by A9, A31, ZF_LANG1:76;
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; :: 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 2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A4;
then A88: X c= L . u by A87;
let u1 be object ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in Union L )
A89: L . u c= Union L by ZF_REFLE:16;
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:15; :: thesis: verum