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 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 & Sum (L (#) F) = Sum (L (#) F) ) by A1, A2; :: thesis: verum