let F, G be FinSequence of INT ; :: thesis: ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G )
assume A1: ( rng F = rng G & F is one-to-one & G is one-to-one ) ; :: thesis: Sum F = Sum G
thus Sum F = addint $$ F by GR_CY_1:2
.= addint $$ G by A1, FINSOP_1:8
.= Sum G by GR_CY_1:2 ; :: thesis: verum