let X, Y be set ; :: thesis: ( X c= Y implies for L being Sequence of X holds L is Sequence of Y )
assume A1: X c= Y ; :: thesis: for L being Sequence of X holds L is Sequence of Y
let L be Sequence of X; :: thesis: L is Sequence of Y
rng L c= X by RELAT_1:def 19;
then rng L c= Y by A1;
hence L is Sequence of Y by RELAT_1:def 19; :: thesis: verum