let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 is increasing implies f2 * f1 is Ordinal-Sequence )
A1: dom (f2 * f1) = f1 " (dom f2) by RELAT_1:147;
assume f1 is increasing ; :: thesis: f2 * f1 is Ordinal-Sequence
then dom (f2 * f1) is Ordinal by A1, Th11;
then reconsider f = f2 * f1 as Sequence by ORDINAL1:def 7;
consider A being Ordinal such that
A2: rng f2 c= A by ORDINAL2:def 4;
rng f c= rng f2 by RELAT_1:26;
then rng f c= A by A2;
hence f2 * f1 is Ordinal-Sequence by ORDINAL2:def 4; :: thesis: verum