A1: rng (s * (canFS A)) c= S ;
rng (canFS A) c= A by FINSEQ_1:def 4;
then s * (canFS A) is FinSequence by FINSEQ_1:16, XBOOLE_1:1;
hence s * (canFS A) is FinSequence of S by A1, FINSEQ_1:def 4; :: thesis: verum