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 non-decreasing 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 non-decreasing ; :: 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