theorem :: MEASURE3:2

for F1, F2 being sequence of ExtREAL st ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) holds
SUM F1 = SUM F2