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

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