for a, b, c being Real_Sequence st ( for n being Nat holds a . n <= (b . n) + (c . n) ) & b is convergent & c is convergent & a is V48() holds
( a is convergent & lim a <= (lim b) + (lim c) )