for F1, F2 being sequence of ExtREAL st F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable holds
F1 is summable