consider p being FinSequence such that
A1: rng p = Carrier LS and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of S by A1, FINSEQ_1:def 4;
take Sum (LS * p) ; :: thesis: ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & Sum (LS * p) = Sum (LS * F) )
thus ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & Sum (LS * p) = Sum (LS * F) ) by A1, A2; :: thesis: verum