theorem :: ORDINAL1:32

for X, Y being set st X c= Y holds
for L being Sequence of X holds L is Sequence of Y