theorem :: RVSUM_3:15

for f1, f2 being real-valued FinSequence st dom f1 = dom f2 & Sum f1 = Sum f2 holds
f1,f2 are_gamma-equivalent by FINSEQ_3:29;