let X, Y be set ; :: thesis: ( X c= Y implies for L being T-Sequence of X holds L is T-Sequence of Y )
assume A1: X c= Y ; :: thesis: for L being T-Sequence of X holds L is T-Sequence of Y
let L be T-Sequence of X; :: thesis: L is T-Sequence of Y
rng L c= X by Def8;
hence rng L c= Y by A1, XBOOLE_1:1; :: according to ORDINAL1:def 8 :: thesis: verum