A1:
rng p2 c= On W
by RELAT_1:def 19;

A2: dom p2 = On W by FUNCT_2:def 1;

dom p1 = On W by FUNCT_2:def 1;

then A3: dom (p1 * p2) = On W by A2, A1, RELAT_1:27;

then reconsider f = p1 * p2 as Sequence by ORDINAL1:def 7;

A4: rng p1 c= On W by RELAT_1:def 19;

rng (p1 * p2) c= rng p1 by RELAT_1:26;

then rng f c= On W by A4;

hence p2 * p1 is Ordinal-Sequence of W by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

A2: dom p2 = On W by FUNCT_2:def 1;

dom p1 = On W by FUNCT_2:def 1;

then A3: dom (p1 * p2) = On W by A2, A1, RELAT_1:27;

then reconsider f = p1 * p2 as Sequence by ORDINAL1:def 7;

A4: rng p1 c= On W by RELAT_1:def 19;

rng (p1 * p2) c= rng p1 by RELAT_1:26;

then rng f c= On W by A4;

hence p2 * p1 is Ordinal-Sequence of W by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum