let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) ) )
assume A1: ( seq1 is bounded & seq2 is bounded ) ; :: thesis: ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )
A2: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2)

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) )
set r1 = lim_sup seq1;
set r2 = lim_sup seq2;
assume that
A3: seq1 is bounded and
A4: seq2 is bounded ; :: thesis: lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2)
for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for k being Nat holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s )
assume 0 < s ; :: thesis: ex n being Nat st
for k being Nat holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
then A5: 0 < s / 2 by XREAL_1:215;
then consider n1 being Nat such that
A6: for k being Nat holds seq1 . (n1 + k) < (lim_sup seq1) + (s / 2) by A3, Th85;
consider n2 being Nat such that
A7: for k being Nat holds seq2 . (n2 + k) < (lim_sup seq2) + (s / 2) by A4, A5, Th85;
for k being Nat holds (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s

proof

let k be Nat; :: thesis: (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
( seq1 . (n1 + (n2 + k)) < (lim_sup seq1) + (s / 2) & seq2 . (n2 + (n1 + k)) < (lim_sup seq2) + (s / 2) ) by A6, A7;
then (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) < ((lim_sup seq1) + (s / 2)) + ((lim_sup seq2) + (s / 2)) by XREAL_1:8;
hence (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s by SEQ_1:7; :: thesis: verum

end;

hence ex n being Nat st
for k being Nat holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s ; :: thesis: verum

end;

hence lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) by A3, A4, Th85; :: thesis: verum

end;

A8: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
(lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2)

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) )
assume that
A9: seq1 is bounded and
A10: seq2 is bounded ; :: thesis: (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2)
lim_sup ((seq1 + seq2) + (- seq1)) <= (lim_sup (- seq1)) + (lim_sup (seq1 + seq2)) by A2, A9, A10;
then lim_sup ((seq1 + seq2) + (- seq1)) <= (- (lim_inf seq1)) + (lim_sup (seq1 + seq2)) by A9, Th90;
then lim_sup ((seq2 + seq1) - seq1) <= (lim_sup (seq1 + seq2)) - (lim_inf seq1) ;
then lim_sup seq2 <= (lim_sup (seq1 + seq2)) - (lim_inf seq1) by Th2;
hence (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) by XREAL_1:19; :: thesis: verum

end;

then A11: (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) by A1;
A12: (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) by A8, A1;
A13: lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) by A2, A1;
A14: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
(lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2)

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) )
set r1 = lim_inf seq1;
set r2 = lim_inf seq2;
assume that
A15: seq1 is bounded and
A16: seq2 is bounded ; :: thesis: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2)
for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k)

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for k being Nat holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) )
assume 0 < s ; :: thesis: ex n being Nat st
for k being Nat holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k)
then A17: 0 < s / 2 by XREAL_1:215;
then consider n1 being Nat such that
A18: for k being Nat holds (lim_inf seq1) - (s / 2) < seq1 . (n1 + k) by A15, Th82;
consider n2 being Nat such that
A19: for k being Nat holds (lim_inf seq2) - (s / 2) < seq2 . (n2 + k) by A16, A17, Th82;
for k being Nat holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k)

proof

let k be Nat; :: thesis: ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k)
( (lim_inf seq1) - (s / 2) < seq1 . (n1 + (n2 + k)) & (lim_inf seq2) - (s / 2) < seq2 . (n2 + (n1 + k)) ) by A18, A19;
then ((lim_inf seq1) - (s / 2)) + ((lim_inf seq2) - (s / 2)) < (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) by XREAL_1:8;
hence ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k) by SEQ_1:7; :: thesis: verum

end;

hence ex n being Nat st
for k being Nat holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) ; :: thesis: verum

end;

hence (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A15, A16, Th82; :: thesis: verum

end;

then A20: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A1;
A21: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2)

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) )
assume that
A22: seq1 is bounded and
A23: seq2 is bounded ; :: thesis: lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2)
lim_inf ((seq1 + seq2) + (- seq2)) >= (lim_inf (seq1 + seq2)) + (lim_inf (- seq2)) by A14, A22, A23;
then lim_inf ((seq1 + seq2) + (- seq2)) >= (lim_inf (seq1 + seq2)) + (- (lim_sup seq2)) by A23, Th90;
then lim_inf ((seq1 + seq2) - seq2) >= (lim_inf (seq1 + seq2)) - (lim_sup seq2) ;
then lim_inf seq1 >= (lim_inf (seq1 + seq2)) - (lim_sup seq2) by Th2;
hence lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) by XREAL_1:20; :: thesis: verum

end;

then A24: lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) by A1;
A25: lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) by A21, A1;
( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) )

proof

assume A26: ( seq1 is convergent or seq2 is convergent ) ; :: thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )

per cases ( seq1 is convergent or seq2 is convergent ) by A26;

suppose seq1 is convergent ; :: thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )

then lim_inf seq1 = lim_sup seq1 by Th88;
hence ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A24, A11, A13, XXREAL_0:1; :: thesis: verum

end;

suppose seq2 is convergent ; :: thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )

then lim_inf seq2 = lim_sup seq2 by Th88;
hence ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A25, A12, A13, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) ) by A14, A21, A2, A8, A1; :: thesis: verum