for n being Nat
for g being FinSequence of REAL n
for h being FinSequence of NAT
for F being FinSequence of REAL n st h is one-to-one & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F