for F, G being FinSequence of INT st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G