let F be sequence of ExtREAL; :: thesis: ( F is V99() implies for n being Element of NAT holds (Ser F) . n <= SUM F )
for n being Element of NAT holds F . n <= F . n ;
hence ( F is V99() implies for n being Element of NAT holds (Ser F) . n <= SUM F ) by Th5; :: thesis: verum