for n being Element of NAT
for f being FinSequence of REAL n
for g being FinSequence of the carrier of (REAL-US n) st f = g holds
Sum f = Sum g