let phi, fi, psi be Ordinal-Sequence; :: thesis: ( fi is increasing & fi is continuous & psi is continuous & phi = psi * fi implies phi is continuous )
assume that
A1: fi is increasing and
A2: for A, B being Ordinal st A in dom fi & A <> 0 & A is limit_ordinal & B = fi . A holds
B is_limes_of fi | A and
A3: for A, B being Ordinal st A in dom psi & A <> 0 & A is limit_ordinal & B = psi . A holds
B is_limes_of psi | A and
A4: phi = psi * fi ; :: according to ORDINAL2:def 13 :: thesis: phi is continuous
let A be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b1 being set holds
( not A in dom phi or A = 0 or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )
let B be Ordinal; :: thesis: ( not A in dom phi or A = 0 or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that
A5: A in dom phi and
A6: A <> 0 and
A7: A is limit_ordinal and
A8: B = phi . A ; :: thesis: B is_limes_of phi | A
reconsider A1 = fi . A as Ordinal ;
A9: fi | A is increasing by A1, Th15;
A10: dom phi c= dom fi by A4, RELAT_1:25;
then A c= dom fi by A5, ORDINAL1:def 2;
then A11: dom (fi | A) = A by RELAT_1:62;
A1 is_limes_of fi | A by A2, A5, A6, A7, A10;
then lim (fi | A) = A1 by ORDINAL2:def 10;
then A12: sup (fi | A) = A1 by A6, A7, A11, A9, Th8;
A13: B = psi . A1 by A4, A5, A8, FUNCT_1:12;
A14: {} in A by A6, ORDINAL3:8;
A15: A1 in dom psi by A4, A5, FUNCT_1:11;
then A1 c= dom psi by ORDINAL1:def 2;
then A16: dom (psi | A1) = A1 by RELAT_1:62;
A17: rng (fi | A) c= sup (rng (fi | A))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (fi | A) or x in sup (rng (fi | A)) )
assume A18: x in rng (fi | A) ; :: thesis: x in sup (rng (fi | A))
then ex y being object st
( y in dom (fi | A) & x = (fi | A) . y ) by FUNCT_1:def 3;
hence x in sup (rng (fi | A)) by A18, ORDINAL2:19; :: thesis: verum
end;
phi | A = psi * (fi | A) by A4, RELAT_1:83;
then A19: phi | A = (psi | A1) * (fi | A) by A17, A12, Lm5;
A c= A1 by A1, A5, A10, Th10;
then B is_limes_of psi | A1 by A3, A7, A13, A15, A11, A14, A9, A12, Th16;
hence B is_limes_of phi | A by A9, A16, A12, A19, Th14; :: thesis: verum