for f, g being XFinSequence of NAT
for i being Integer st dom f = dom g & ( for n being object st n in dom f holds
f . n = i * (g . n) ) holds
Sum f = i * (Sum g)