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) )

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

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

A5:
b + c is convergent
by A2;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;a . n <= (b . n) + (c . n) by A1;

hence a . n <= (b + c) . n by SEQ_1:7; :: thesis: verum

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