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 RELAT_1:def 19;
then rng L c= Y by A1, XBOOLE_1:1;
hence L is T-Sequence of Y by RELAT_1:def 19; :: thesis: verum