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