let W be Universe; :: thesis: for L being DOMAIN-Sequence of 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 ; :: 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
A6: 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
A7: ( u in dom L & X in L . u ) by Lm1;
reconsider u = u as Ordinal by A7;
u in On W by A7, ZF_REFLE:def 5;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
L . u is epsilon-transitive by A4;
then A8: X c= L . u by A7, ORDINAL1:def 2;
let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in Union L )
assume u1 in X ; :: thesis: u1 in Union L
then ( u1 in L . u & L . u c= Union L ) by A8, ZF_REFLE:24;
hence u1 in Union L ; :: thesis: verum

end;

set M = Union L;

now

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
A9: {(x. 0 ),(x. 1),(x. 2)} misses Free H and
A10: 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
A11: 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));
( 0 <= 5 & k + 0 = k ) ;
then A12: not x. (k + 5) in variables_in H by A11, XREAL_1:9;
then A13: {(x. 0 ),(x. 1),(x. 2)} misses Free (H / (x. 0 ),(x. (k + 5))) by A9, A10, Lm2;
A14: ( 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 A9, A10, A12, Lm2;
x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A15: not x. 0 in Free (H / (x. 0 ),(x. (k + 5))) by A13, XBOOLE_0:3;
set F = def_func' H,f;
defpred S₁[ set , set ] means $1 in L . $2;
A16: 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
A17: ( u in dom L & d in L . u ) by Lm1;
u in On W by A17, 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 A17; :: thesis: verum

end;

consider g being Function such that
A18: ( 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(A16);
let u be Element of Union L; :: thesis: (def_func' H,f) .: u in Union L
( u in W & 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 u in card W & card (g .: ((def_func' H,f) .: u)) c= card u & card (g .: u) c= card u ) by CARD_2:3, CLASSES2:1, XBOOLE_1:1;
then A19: ( card (g .: ((def_func' H,f) .: u)) in card W & card (g .: u) in card W & W is Tarski ) by ORDINAL1:22;
A20: 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
A21: ( u2 in dom g & u1 = g . u2 ) by FUNCT_1:def 5;
reconsider d = u2 as Element of Union L by A18, A21;
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 A18;
hence u1 in W by A21; :: thesis: verum

end;

g .: ((def_func' H,f) .: u) c= rng g by RELAT_1:144;
then g .: ((def_func' H,f) .: u) c= W by A20, XBOOLE_1:1;
then g .: ((def_func' H,f) .: u) in W by A19, CLASSES1:2;
then sup (g .: ((def_func' H,f) .: u)) in W by ZF_REFLE:28;
then reconsider b1 = sup (g .: ((def_func' H,f) .: u)) as Ordinal of W ;
consider b0 being Ordinal of W such that
A22: ( b0 = g . u & u in L . b0 & ( for b being Ordinal of W st u in L . b holds
b0 c= b ) ) by A18;
( card VAR = omega & omega in card W ) by A1, CARD_1:21, CARD_1:84, CLASSES2:1, ZF_REFLE:25;
then ( card (f .: (dom f)) c= card (dom f) & card (dom f) in card W & rng f = f .: (dom f) ) by CARD_2:3, FUNCT_2:def 1, RELAT_1:146;
then ( card (g .: (rng f)) c= card (rng f) & card (rng f) in card W & g .: (rng f) c= rng g ) by CARD_2:3, ORDINAL1:22, RELAT_1:144;
then ( card (g .: (rng f)) in card W & g .: (rng f) c= W ) by A20, ORDINAL1:22, XBOOLE_1:1;
then g .: (rng f) in W by CLASSES1:2;
then sup (g .: (rng f)) in W by ZF_REFLE:28;
then reconsider b2 = sup (g .: (rng f)) as Ordinal of W ;
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 A24: ( X c= Union L & 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 A25: 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
A26: ( b = g . d & d in L . b & ( for a being Ordinal of W st d in L . a holds
b c= a ) ) by A18;
b in g .: X by A18, A25, A26, FUNCT_1:def 12;
then b in sup (g .: X) by ORDINAL2:27;
then L . b c= L . a by A2, A24;
hence u1 in L . a by A26; :: thesis: verum

end;

set b = b0 \/ b1;
set a = (b0 \/ b1) \/ b2;
consider phi being Ordinal-Sequence of W such that
A27: ( phi is increasing & phi is continuous ) and
A28: 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
A29: ( (b0 \/ b1) \/ b2 in a1 & phi . a1 = a1 ) by A1, A27, ZFREFLE1:30;
A30: dom f = VAR by FUNCT_2:def 1;
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 )
assume A31: u in rng f ; :: thesis: u in L . a1
then consider u1 being set such that
A32: ( u1 in dom f & u = f . u1 ) by FUNCT_1:def 5;
reconsider u1 = u1 as Variable by A32;
consider a2 being Ordinal of W such that
A33: ( a2 = g . (f . u1) & f . u1 in L . a2 & ( for b being Ordinal of W st f . u1 in L . b holds
a2 c= b ) ) by A18;
a2 in g .: (rng f) by A18, A31, A32, A33, FUNCT_1:def 12;
then ( a2 in b2 & b2 c= (b0 \/ b1) \/ b2 ) by ORDINAL2:27, XBOOLE_1:7;
then L . a2 c= L . a1 by A2, A29, ORDINAL1:19;
hence u in L . a1 by A32, A33; :: thesis: verum

end;

then reconsider v = f as Function of VAR ,(L . a1) by A30, FUNCT_2:def 1, RELSET_1:11;
A34: L . a1 in Union L by A4;
( (def_func' H,f) .: u c= Union L & sup (g .: ((def_func' H,f) .: u)) c= b0 \/ b1 & b0 \/ b1 in a1 ) by A29, ORDINAL1:22, XBOOLE_1:7;
then ( (def_func' H,f) .: u c= L . (b0 \/ b1) & L . (b0 \/ b1) c= L . a1 ) by A2, A23;
then A35: (def_func' H,f) .: u c= L . a1 by XBOOLE_1:1;
( 0 < 5 & k + 0 = k ) ;
then A36: ( 0 <= k & k < k + 5 ) by NAT_1:2, XREAL_1:8;
then A37: not x. 0 in variables_in (H / (x. 0 ),(x. (k + 5))) by ZF_LANG1:86, ZF_LANG1:198;
set x = x. (k + 10);
set q = Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )));
( 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 A38: L . b0 c= L . a1 by A2, A29, ORDINAL1:22;
then reconsider mu = u as Element of L . a1 by A22;
set w = (v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu;
A39: ( 10 > 0 & 10 > 3 & 10 <= 10 + k & 10 + k = k + 10 ) by NAT_1:11;
then A40: ( x. 0 <> x. 3 & x. (k + 10) <> x. 0 & x. (k + 10) <> x. 3 ) by ZF_LANG1:86;
A41: ( 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 )} & variables_in (H / (x. 0 ),(x. (k + 5))) c= ((variables_in H) \ {(x. 0 )}) \/ {(x. (k + 5))} ) by ZF_LANG1:201;
( 0 <= 10 & k + 0 = k & 5 < 10 ) ;
then ( not k + 10 < k & k + 5 < k + 10 ) by XREAL_1:8;
then ( not x. (k + 10) in variables_in H & k + 5 <> k + 10 ) by A11;
then ( not x. (k + 10) in (variables_in H) \ {(x. 0 )} & x. (k + 10) <> x. (k + 5) & ( x. (k + 10) <> x. (k + 5) implies not x. (k + 10) in {(x. (k + 5))} ) ) by TARSKI:def 1, XBOOLE_0:def 5, ZF_LANG1:86;
then not x. (k + 10) in variables_in (H / (x. 0 ),(x. (k + 5))) by A41, XBOOLE_0:def 3;
then ( not x. (k + 10) in (variables_in (H / (x. 0 ),(x. (k + 5)))) \ {(x. 4)} & not x. (k + 10) in {(x. 0 )} ) by A40, TARSKI:def 1, XBOOLE_0:def 5;
then A42: not x. (k + 10) in variables_in ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) by A41, XBOOLE_0:def 3;
(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 A43: 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)

( not k + 5 < k & not k + 10 < k & 4 <> k + 5 ) by NAT_1:11;
then ( not x. (k + 5) in variables_in H & not x. (k + 10) in variables_in H & x. (k + 5) <> x. 0 & x. (k + 10) <> x. 0 & x. (k + 5) <> x. 4 ) by A11, A36, A39, ZF_LANG1:86;
then A44: x. 0 in Free (Ex (x. 3),(((x. 3) 'in' (x. (k + 10))) '&' ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )))) by A43, Lm5;
A45: (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 A46: 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
A47: ( u2 in dom (def_func' H,f) & u2 in u & u1 = (def_func' H,f) . u2 ) by FUNCT_1:def 12;
reconsider u2 = u2 as Element of Union L by A47;
( 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 & 0 <> 4 ) by A14, A15, ZFMODEL2:11, FUNCT_7:130;
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 ) & x. 0 <> x. 4 ) by A37, ZFMODEL2:14, ZF_LANG1:86;
then ( 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 ) & not x. 4 in variables_in ((H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 )) ) by FUNCT_7:35, ZF_LANG1:198;
then A48: Union L,(f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2) |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by ZFMODEL2:6;
reconsider m1 = u1 as Element of L . a1 by A35, A46;
L . a1 is epsilon-transitive by A4;
then u c= L . a1 by A22, A38, ORDINAL1:def 2;
then reconsider m2 = u2 as Element of L . a1 by A47;
( (f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2) = (v / (x. 3),m2) / (x. 0 ),m1 & L . a1 c= Union L ) by A47, ZF_REFLE:24;
then (f / (x. 3),u2) / (x. 0 ),((def_func' H,f) . u2) = (Union L) ! ((v / (x. 3),m2) / (x. 0 ),m1) by ZF_LANG1:def 2;
then L . a1,(v / (x. 3),m2) / (x. 0 ),m1 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A28, A29, A48;
then ( L . a1,((v / (x. 3),m2) / (x. 0 ),m1) / (x. (k + 10)),mu |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) & ((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1 = (v / (x. (k + 10)),mu) / (x. 0 ),m1 ) by A42, ZFMODEL2:6, ZFMODEL2:9;
then A49: 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 A40, ZFMODEL2:7;
( ((((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)) & ((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 A40, FUNCT_7:34, FUNCT_7:130;
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)) by A47, ZF_MODEL:13;
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 A49, 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 A44, 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 )
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 A44, Def1;
then consider m1 being Element of L . a1 such that
A50: ( u1 = m1 & 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
A51: 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 A50, ZF_LANG1:82;
A52: ( L . a1,(((v / (x. 0 ),(v . (x. 4))) / (x. (k + 10)),mu) / (x. 0 ),m1) / (x. 3),m2 |= (x. 3) 'in' (x. (k + 10)) & ((((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)) & ((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 & 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 A40, A51, FUNCT_7:34, FUNCT_7:130, ZF_MODEL:15;
then A53: m2 in u by 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. 3),m2) / (x. 0 ),m1) / (x. (k + 10)),mu |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A40, A52, ZFMODEL2:7;
then A54: L . a1,(v / (x. 3),m2) / (x. 0 ),m1 |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) by A42, ZFMODEL2:6;
( m1 in L . a1 & m2 in L . a1 & L . a1 c= Union L ) by ZF_REFLE:24;
then reconsider u' = m1, u2 = m2 as Element of Union L ;
( (f / (x. 3),u2) / (x. 0 ),u' = (v / (x. 3),m2) / (x. 0 ),m1 & L . a1 c= Union L & 0 <> 4 ) by ZF_REFLE:24;
then ( (f / (x. 3),u2) / (x. 0 ),u' = (Union L) ! ((v / (x. 3),m2) / (x. 0 ),m1) & x. 0 <> x. 4 ) by ZF_LANG1:86, ZF_LANG1:def 2;
then ( Union L,(f / (x. 3),u2) / (x. 0 ),u' |= (H / (x. 0 ),(x. (k + 5))) / (x. 4),(x. 0 ) & ((f / (x. 3),u2) / (x. 0 ),u') / (x. 4),u' = ((f / (x. 3),u2) / (x. 4),u') / (x. 0 ),u' & ((f / (x. 3),u2) / (x. 0 ),u') . (x. 0 ) = u' ) by A28, A29, A54, FUNCT_7:35, FUNCT_7:130;
then Union L,((f / (x. 3),u2) / (x. 4),u') / (x. 0 ),u' |= H / (x. 0 ),(x. (k + 5)) by A37, ZFMODEL2:13;
then Union L,(f / (x. 3),u2) / (x. 4),u' |= H / (x. 0 ),(x. (k + 5)) by A37, ZFMODEL2:6;
then ( (def_func' H,f) . u2 = u' & dom (def_func' H,f) = Union L ) by A14, A15, FUNCT_2:def 1, ZFMODEL2:11;
hence u1 in (def_func' H,f) .: u by A50, A53, 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 A45, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A55: 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)

( not k + 5 < k & not k + 10 < k & 4 <> k + 5 ) by NAT_1:11;
then ( not x. (k + 5) in variables_in H & not x. (k + 10) in variables_in H & x. (k + 5) <> x. 0 & x. (k + 10) <> x. 0 & x. (k + 5) <> x. 4 ) by A11, A36, A39, 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 A55, Lm5;
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 A10, A55, Lm4; :: 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;

hence (def_func' H,f) .: u in Union L by A5, A34, Def2; :: 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