let L be Ordinal-Sequence; :: thesis: for A being Ordinal holds L | (Rank A) is Ordinal-Sequence
let A be Ordinal; :: thesis: L | (Rank A) is Ordinal-Sequence
reconsider K = L | (Rank A) as Sequence by Th8;
consider B being Ordinal such that
A1: rng L c= B by ORDINAL2:def 4;
rng K c= rng L by RELAT_1:70;
then rng K c= B by A1;
hence L | (Rank A) is Ordinal-Sequence by ORDINAL2:def 4; :: thesis: verum