consider F being FinSequence such that

A1: rng F = Carrier L and

A2: F is one-to-one by FINSEQ_4:58;

reconsider F = F as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;

take Sum (L (#) F) ; :: thesis: ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )

take F ; :: thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )

thus ( F is one-to-one & rng F = Carrier L ) by A1, A2; :: thesis: Sum (L (#) F) = Sum (L (#) F)

thus Sum (L (#) F) = Sum (L (#) F) ; :: thesis: verum

A1: rng F = Carrier L and

A2: F is one-to-one by FINSEQ_4:58;

reconsider F = F as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;

take Sum (L (#) F) ; :: thesis: ex F being FinSequence of V st

( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )

take F ; :: thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )

thus ( F is one-to-one & rng F = Carrier L ) by A1, A2; :: thesis: Sum (L (#) F) = Sum (L (#) F)

thus Sum (L (#) F) = Sum (L (#) F) ; :: thesis: verum