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

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