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

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