consider k being Nat such that

A1: dom (Sgm N) = Seg k by FINSEQ_1:def 2;

consider l being Nat such that

A2: dom s = Seg l by FINSEQ_1:def 2;

rng (Sgm N) = N by A2, FINSEQ_1:def 13;

then dom (s * (Sgm N)) = dom (Sgm N) by RELAT_1:27;

hence s * (Sgm N) is FinSequence-like by A1, FINSEQ_1:def 2; :: thesis: verum

A1: dom (Sgm N) = Seg k by FINSEQ_1:def 2;

consider l being Nat such that

A2: dom s = Seg l by FINSEQ_1:def 2;

rng (Sgm N) = N by A2, FINSEQ_1:def 13;

then dom (s * (Sgm N)) = dom (Sgm N) by RELAT_1:27;

hence s * (Sgm N) is FinSequence-like by A1, FINSEQ_1:def 2; :: thesis: verum