theorem Th30: :: RLAFFIN1:30

for S being non empty addLoopStr
for LS being Linear_Combination of S
for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds
sum LS = Sum (LS * F)