let a, b, c be Real_Sequence; :: thesis: ( ( for n being Nat holds a . n <= (b . n) + (c . n) ) & b is convergent & c is convergent & a is V48() implies ( a is convergent & lim a <= (lim b) + (lim c) ) )
assume that
A1: for n being Nat holds a . n <= (b . n) + (c . n) and
A2: ( b is convergent & c is convergent ) and
A3: a is V48() ; :: thesis: ( a is convergent & lim a <= (lim b) + (lim c) )
A4: now :: thesis: for n being Nat holds a . n <= (b + c) . n
let n be Nat; :: thesis: a . n <= (b + c) . n
a . n <= (b . n) + (c . n) by A1;
hence a . n <= (b + c) . n by SEQ_1:7; :: thesis: verum
end;
A5: b + c is convergent by A2;
hence a is convergent by A3, A4, Th8; :: thesis: lim a <= (lim b) + (lim c)
lim (b + c) = (lim b) + (lim c) by A2, SEQ_2:6;
hence lim a <= (lim b) + (lim c) by A3, A5, A4, Th8; :: thesis: verum