consider A being Ordinal;
consider L being T-Sequence of A;
reconsider K = L as T-Sequence ;
take K ; :: thesis: K is Ordinal-yielding
take A ; :: according to ORDINAL2:def 8 :: thesis: rng K c= A
thus rng K c= A by ORDINAL1:def 8; :: thesis: verum