for F, G being FinSequence of ExtREAL
for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds
Sum F = Sum G