consider F being FinSequence such that

A1: ( rng F = Carrier l & F is one-to-one ) by FINSEQ_4:58;

reconsider F = F as FinSequence of L by A1, FINSEQ_1:def 4;

take Sum (ScFS (v,l,F)) ; :: thesis: ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) )

take F ; :: thesis: ( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) )

thus ( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) ) by A1; :: thesis: verum

A1: ( rng F = Carrier l & F is one-to-one ) by FINSEQ_4:58;

reconsider F = F as FinSequence of L by A1, FINSEQ_1:def 4;

take Sum (ScFS (v,l,F)) ; :: thesis: ex F being FinSequence of L st

( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) )

take F ; :: thesis: ( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) )

thus ( F is one-to-one & rng F = Carrier l & Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F)) ) by A1; :: thesis: verum