theorem Th9: :: ORDERS_5:8

for X being set
for s, t being FinSequence of X
for f being Function of X,REAL st s is one-to-one & t is one-to-one & rng t c= rng s & ( for x being Element of X st x in (rng s) \ (rng t) holds
f . x = 0 ) holds
Sum (f * s) = Sum (f * t)