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