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