let F1, F2 be sequence of ExtREAL; :: thesis: ( ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) implies SUM F1 = SUM F2 )

assume A1: for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ; :: thesis: SUM F1 = SUM F2

then for n being Element of NAT holds (Ser F2) . n <= (Ser F1) . n ;

then A2: SUM F2 <= SUM F1 by Th1;

for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n by A1;

then SUM F1 <= SUM F2 by Th1;

hence SUM F1 = SUM F2 by A2, XXREAL_0:1; :: thesis: verum

assume A1: for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ; :: thesis: SUM F1 = SUM F2

then for n being Element of NAT holds (Ser F2) . n <= (Ser F1) . n ;

then A2: SUM F2 <= SUM F1 by Th1;

for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n by A1;

then SUM F1 <= SUM F2 by Th1;

hence SUM F1 = SUM F2 by A2, XXREAL_0:1; :: thesis: verum