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 (DivisibleMod L) by A1, FINSEQ_1:def 4;
take Sum (ScFS (v,l,F)) ; :: thesis: ex F being FinSequence of (DivisibleMod 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