let seq1, seq2 be ExtREAL_sequence; :: thesis:
let r be R_eal; :: thesis:
assume that
A0: r in REAL and
A1: for n being Nat holds seq1 . n = r + (seq2 . n) ; :: thesis:
reconsider R1 = rng (inferior_realsequence seq1), R2 = rng (inferior_realsequence seq2), P1 = rng (superior_realsequence seq1), P2 = rng (superior_realsequence seq2) as non empty Subset of ExtREAL ;

let z be set ; :: thesis:
assume z in R1 ; :: thesis:
then consider n being set such that
B1: ( n in NAT & (inferior_realsequence seq1) . n = z ) by FUNCT_2:17;
reconsider n = n as Element of NAT by B1;
consider Y1 being non empty Subset of ExtREAL such that
B2: ( Y1 = { (seq1 . k) where k is Element of NAT : n <= k } & z = inf Y1 ) by B1, RINFSUP2:def 6;
consider Y2 being non empty Subset of ExtREAL such that
B21: ( Y2 = { (seq2 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq2) . n = inf Y2 ) by RINFSUP2:def 6;

let w be set ; :: thesis:
assume w in Y1 ; :: thesis:
then consider k1 being Element of NAT such that
B3: ( w = seq1 . k1 & n <= k1 ) by B2;
reconsider w1 = w as R_eal by B3;
B4: w1 = r + (seq2 . k1) by A1, B3;
( r in {r} & seq2 . k1 in Y2 ) by B3, B21, TARSKI:def 1;
hence w in {r} + Y2 by B4, SUPINF_2:def 5; :: thesis:

end;

then B6: Y1 c= {r} + Y2 by TARSKI:def 3;

let w be set ; :: thesis:
assume w in {r} + Y2 ; :: thesis:
then consider w1, w2 being R_eal such that
B7: ( w1 in {r} & w2 in Y2 & w = w1 + w2 ) by SUPINF_2:def 5;
consider k2 being Element of NAT such that
B8: ( w2 = seq2 . k2 & n <= k2 ) by B21, B7;
w1 = r by B7, TARSKI:def 1;
then w = seq1 . k2 by A1, B7, B8;
hence w in Y1 by B2, B8; :: thesis:

end;

then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by B6, XBOOLE_0:def 10;
then inf Y1 = (inf {r}) + (inf Y2) by A0, SUPINF227a;
then B9: inf Y1 = r + (inf Y2) by XXREAL_2:13;
( r in {r} & (inferior_realsequence seq2) . n in R2 ) by FUNCT_2:6, TARSKI:def 1;
hence z in {r} + R2 by B9, B2, B21, SUPINF_2:def 5; :: thesis:

end;

then B9: R1 c= {r} + R2 by TARSKI:def 3;

let z be set ; :: thesis:
assume z in {r} + R2 ; :: thesis:
then consider z2, z3 being R_eal such that
C2: ( z2 in {r} & z3 in R2 & z = z2 + z3 ) by SUPINF_2:def 5;
consider n being set such that
C3: ( n in NAT & (inferior_realsequence seq2) . n = z3 ) by C2, FUNCT_2:17;
reconsider n = n as Element of NAT by C3;
consider Y2 being non empty Subset of ExtREAL such that
C4: ( Y2 = { (seq2 . k) where k is Element of NAT : n <= k } & z3 = inf Y2 ) by C3, RINFSUP2:def 6;
consider Y1 being non empty Subset of ExtREAL such that
C5: ( Y1 = { (seq1 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq1) . n = inf Y1 ) by RINFSUP2:def 6;

let w be set ; :: thesis:
assume w in Y1 ; :: thesis:
then consider k1 being Element of NAT such that
B3: ( w = seq1 . k1 & n <= k1 ) by C5;
reconsider w1 = w as R_eal by B3;
B4: w1 = r + (seq2 . k1) by A1, B3;
( r in {r} & seq2 . k1 in Y2 ) by B3, C4, TARSKI:def 1;
hence w in {r} + Y2 by B4, SUPINF_2:def 5; :: thesis:

end;

then B6: Y1 c= {r} + Y2 by TARSKI:def 3;

let w be set ; :: thesis:
assume w in {r} + Y2 ; :: thesis:
then consider w1, w2 being R_eal such that
B7: ( w1 in {r} & w2 in Y2 & w = w1 + w2 ) by SUPINF_2:def 5;
consider k2 being Element of NAT such that
B8: ( w2 = seq2 . k2 & n <= k2 ) by C4, B7;
w1 = r by B7, TARSKI:def 1;
then w = seq1 . k2 by A1, B7, B8;
hence w in Y1 by C5, B8; :: thesis:

end;

then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by B6, XBOOLE_0:def 10;
then inf Y1 = (inf {r}) + (inf Y2) by A0, SUPINF227a;
then inf Y1 = r + (inf Y2) by XXREAL_2:13;
then z = (inferior_realsequence seq1) . n by C2, C4, C5, TARSKI:def 1;
hence z in R1 by FUNCT_2:6; :: thesis:

end;

then {r} + R2 c= R1 by TARSKI:def 3;
then R1 = {r} + R2 by B9, XBOOLE_0:def 10;
then sup R1 = (sup {r}) + (sup R2) by A0, SUPINF226a;
hence lim_inf seq1 = r + (lim_inf seq2) by XXREAL_2:11; :: thesis:

let z be set ; :: thesis:
assume z in P1 ; :: thesis:
then consider n being set such that
B1: ( n in NAT & (superior_realsequence seq1) . n = z ) by FUNCT_2:17;
reconsider n = n as Element of NAT by B1;
consider Y1 being non empty Subset of ExtREAL such that
B2: ( Y1 = { (seq1 . k) where k is Element of NAT : n <= k } & z = sup Y1 ) by B1, RINFSUP2:def 7;
consider Y2 being non empty Subset of ExtREAL such that
B21: ( Y2 = { (seq2 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq2) . n = sup Y2 ) by RINFSUP2:def 7;

end;

then B6: Y1 c= {r} + Y2 by TARSKI:def 3;

end;

then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by B6, XBOOLE_0:def 10;
then sup Y1 = (sup {r}) + (sup Y2) by A0, SUPINF226a;
then B9: sup Y1 = r + (sup Y2) by XXREAL_2:11;
( r in {r} & (superior_realsequence seq2) . n in P2 ) by FUNCT_2:6, TARSKI:def 1;
hence z in {r} + P2 by B9, B2, B21, SUPINF_2:def 5; :: thesis:

end;

then B9: P1 c= {r} + P2 by TARSKI:def 3;

let z be set ; :: thesis:
assume z in {r} + P2 ; :: thesis:
then consider z2, z3 being R_eal such that
C2: ( z2 in {r} & z3 in P2 & z = z2 + z3 ) by SUPINF_2:def 5;
consider n being set such that
C3: ( n in NAT & (superior_realsequence seq2) . n = z3 ) by C2, FUNCT_2:17;
reconsider n = n as Element of NAT by C3;
consider Y2 being non empty Subset of ExtREAL such that
C4: ( Y2 = { (seq2 . k) where k is Element of NAT : n <= k } & z3 = sup Y2 ) by C3, RINFSUP2:def 7;
consider Y1 being non empty Subset of ExtREAL such that
C5: ( Y1 = { (seq1 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq1) . n = sup Y1 ) by RINFSUP2:def 7;

end;

then B6: Y1 c= {r} + Y2 by TARSKI:def 3;

let w be set ; :: thesis:
assume w in {r} + Y2 ; :: thesis:
then consider w1, w2 being R_eal such that
B7: ( w1 in {r} & w2 in Y2 & w = w1 + w2 ) by SUPINF_2:def 5;
consider k2 being Element of NAT such that
B8: ( w2 = seq2 . k2 & n <= k2 ) by C4, B7;
w1 = r by B7, TARSKI:def 1;
then w = seq1 . k2 by A1, B7, B8;
hence w in Y1 by C5, B8; :: thesis:

end;

then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by B6, XBOOLE_0:def 10;
then sup Y1 = (sup {r}) + (sup Y2) by A0, SUPINF226a;
then sup Y1 = r + (sup Y2) by XXREAL_2:11;
then z = (superior_realsequence seq1) . n by C2, C4, C5, TARSKI:def 1;
hence z in P1 by FUNCT_2:6; :: thesis:

end;

then {r} + P2 c= P1 by TARSKI:def 3;
then P1 = {r} + P2 by B9, XBOOLE_0:def 10;
then inf P1 = (inf {r}) + (inf P2) by A0, SUPINF227a;
hence lim_sup seq1 = r + (lim_sup seq2) by XXREAL_2:13; :: thesis: