let f1, f2 be FinSequence of REAL ; :: thesis: ( f2 = f1 - {0} implies Sum f1 = Sum f2 )
A1: (dom f1) \ (f1 " {0}) c= dom f1 by XBOOLE_1:36;
assume f2 = f1 - {0} ; :: thesis: Sum f1 = Sum f2
hence Sum f1 = Sum f2 by A1, Th11; :: thesis: verum