consider F being FinSequence such that

A2: rng F = Carrier L and

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

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

take Sum (L (#) F) ; :: thesis: ex F being FinSequence of the carrier 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 A2, A3; :: thesis: Sum (L (#) F) = Sum (L (#) F)

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

A2: rng F = Carrier L and

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

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

take Sum (L (#) F) ; :: thesis: ex F being FinSequence of the carrier 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 A2, A3; :: thesis: Sum (L (#) F) = Sum (L (#) F)

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