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