let X be set ; :: thesis: for L being T-Sequence of X
for A being Ordinal holds L | A is T-Sequence of X
let L be T-Sequence of X; :: thesis: for A being Ordinal holds L | A is T-Sequence of X
let A be Ordinal; :: thesis: L | A is T-Sequence of X
rng L c= X by Def8;
hence L | A is T-Sequence of X by Th47; :: thesis: verum