let a, b, c be Real_Sequence; :: thesis: ( ( for n being Element of 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 Element of NAT holds a . n <= (b . n) + (c . n) and
A2: b is convergent and
A3: c is convergent and
A4: a is non-decreasing ; :: thesis: ( a is convergent & lim a <= (lim b) + (lim c) )
A5: b + c is convergent by A2, A3, SEQ_2:19;

A6: now

let n be Element of NAT ; :: thesis: a . n <= (b + c) . n
a . n <= (b . n) + (c . n) by A1;
hence a . n <= (b + c) . n by SEQ_1:11; :: thesis: verum

end;

A7: lim (b + c) = (lim b) + (lim c) by A2, A3, SEQ_2:20;
thus a is convergent by A4, A5, A6, Th8; :: thesis: lim a <= (lim b) + (lim c)
thus lim a <= (lim b) + (lim c) by A4, A5, A6, A7, Th8; :: thesis: verum