consider k being Nat such that
A1: dom (idseq (len s)) = Seg k by FINSEQ_1:def 2;
rng (idseq (len s)) = rng (id (Seg (len s))) by FINSEQ_2:def 1
.= dom s by FINSEQ_1:def 3 ;
then dom (s * (idseq (len s))) = dom (idseq (len s)) by RELAT_1:27;
hence s * (idseq (len s)) is FinSequence-like by A1, FINSEQ_1:def 2; :: thesis: verum