theorem EQSUMLF: :: ZMODLAT2:1

for K being Ring
for V being LeftMod of K
for L being Function of the carrier of V, the carrier of K
for A being Subset of V
for F, F1 being FinSequence of the carrier of V st F is one-to-one & rng F = A & F1 is one-to-one & rng F1 = A holds
Sum (L (#) F) = Sum (L (#) F1)