let seq1, seq2 be ExtREAL_sequence; :: thesis: for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )
let r be R_eal; :: thesis: ( r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) implies ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) )
assume that
A1: r in REAL and
A2: for n being Nat holds seq1 . n = r + (seq2 . n) ; :: thesis: ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )
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 ;
now :: thesis: for z being object st z in {r} + R2 holds
z in R1
let z be object ; :: thesis: ( z in {r} + R2 implies z in R1 )
assume z in {r} + R2 ; :: thesis: z in R1
then consider z2, z3 being R_eal such that
A3: z = z2 + z3 and
A4: z2 in {r} and
A5: z3 in R2 ;
consider n being object such that
A6: n in NAT and
A7: (inferior_realsequence seq2) . n = z3 by A5, FUNCT_2:11;
reconsider n = n as Element of NAT by A6;
consider Y2 being non empty Subset of ExtREAL such that
A8: Y2 = { (seq2 . k) where k is Nat : n <= k } and
A9: z3 = inf Y2 by A7, RINFSUP2:def 6;
consider Y1 being non empty Subset of ExtREAL such that
A10: Y1 = { (seq1 . k) where k is Nat : n <= k } and
A11: (inferior_realsequence seq1) . n = inf Y1 by RINFSUP2:def 6;
now :: thesis: for w being object st w in Y1 holds
w in {r} + Y2
let w be object ; :: thesis: ( w in Y1 implies w in {r} + Y2 )
A12: r in {r} by TARSKI:def 1;
assume w in Y1 ; :: thesis: w in {r} + Y2
then consider k1 being Nat such that
A13: w = seq1 . k1 and
A14: n <= k1 by A10;
reconsider w1 = w as R_eal by A13;
A15: seq2 . k1 in Y2 by A8, A14;
w1 = r + (seq2 . k1) by A2, A13;
hence w in {r} + Y2 by A12, A15; :: thesis: verum
end;
then A16: Y1 c= {r} + Y2 by TARSKI:def 3;
now :: thesis: for w being object st w in {r} + Y2 holds
w in Y1
let w be object ; :: thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; :: thesis: w in Y1
then consider w1, w2 being R_eal such that
A17: w = w1 + w2 and
A18: w1 in {r} and
A19: w2 in Y2 ;
consider k2 being Nat such that
A20: w2 = seq2 . k2 and
A21: n <= k2 by A8, A19;
w1 = r by A18, TARSKI:def 1;
then w = seq1 . k2 by A2, A17, A20;
hence w in Y1 by A10, A21; :: thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A16, XBOOLE_0:def 10;
then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9;
then inf Y1 = r + (inf Y2) by XXREAL_2:13;
then z = (inferior_realsequence seq1) . n by A4, A3, A9, A11, TARSKI:def 1;
hence z in R1 by FUNCT_2:4; :: thesis: verum
end;
then A22: {r} + R2 c= R1 by TARSKI:def 3;
now :: thesis: for z being object st z in {r} + P2 holds
z in P1
let z be object ; :: thesis: ( z in {r} + P2 implies z in P1 )
assume z in {r} + P2 ; :: thesis: z in P1
then consider z2, z3 being R_eal such that
A23: z = z2 + z3 and
A24: z2 in {r} and
A25: z3 in P2 ;
consider n being object such that
A26: n in NAT and
A27: (superior_realsequence seq2) . n = z3 by A25, FUNCT_2:11;
reconsider n = n as Element of NAT by A26;
consider Y2 being non empty Subset of ExtREAL such that
A28: Y2 = { (seq2 . k) where k is Nat : n <= k } and
A29: z3 = sup Y2 by A27, RINFSUP2:def 7;
consider Y1 being non empty Subset of ExtREAL such that
A30: Y1 = { (seq1 . k) where k is Nat : n <= k } and
A31: (superior_realsequence seq1) . n = sup Y1 by RINFSUP2:def 7;
now :: thesis: for w being object st w in Y1 holds
w in {r} + Y2
let w be object ; :: thesis: ( w in Y1 implies w in {r} + Y2 )
A32: r in {r} by TARSKI:def 1;
assume w in Y1 ; :: thesis: w in {r} + Y2
then consider k1 being Nat such that
A33: w = seq1 . k1 and
A34: n <= k1 by A30;
reconsider w1 = w as R_eal by A33;
A35: seq2 . k1 in Y2 by A28, A34;
w1 = r + (seq2 . k1) by A2, A33;
hence w in {r} + Y2 by A32, A35; :: thesis: verum
end;
then A36: Y1 c= {r} + Y2 by TARSKI:def 3;
now :: thesis: for w being object st w in {r} + Y2 holds
w in Y1
let w be object ; :: thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; :: thesis: w in Y1
then consider w1, w2 being R_eal such that
A37: w = w1 + w2 and
A38: w1 in {r} and
A39: w2 in Y2 ;
consider k2 being Nat such that
A40: w2 = seq2 . k2 and
A41: n <= k2 by A28, A39;
w1 = r by A38, TARSKI:def 1;
then w = seq1 . k2 by A2, A37, A40;
hence w in Y1 by A30, A41; :: thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A36, XBOOLE_0:def 10;
then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8;
then sup Y1 = r + (sup Y2) by XXREAL_2:11;
then z = (superior_realsequence seq1) . n by A24, A23, A29, A31, TARSKI:def 1;
hence z in P1 by FUNCT_2:4; :: thesis: verum
end;
then A42: {r} + P2 c= P1 by TARSKI:def 3;
now :: thesis: for z being object st z in R1 holds
z in {r} + R2
let z be object ; :: thesis: ( z in R1 implies z in {r} + R2 )
assume z in R1 ; :: thesis: z in {r} + R2
then consider n being object such that
A43: n in NAT and
A44: (inferior_realsequence seq1) . n = z by FUNCT_2:11;
reconsider n = n as Element of NAT by A43;
consider Y1 being non empty Subset of ExtREAL such that
A45: Y1 = { (seq1 . k) where k is Nat : n <= k } and
A46: z = inf Y1 by A44, RINFSUP2:def 6;
consider Y2 being non empty Subset of ExtREAL such that
A47: Y2 = { (seq2 . k) where k is Nat : n <= k } and
A48: (inferior_realsequence seq2) . n = inf Y2 by RINFSUP2:def 6;
now :: thesis: for w being object st w in Y1 holds
w in {r} + Y2
let w be object ; :: thesis: ( w in Y1 implies w in {r} + Y2 )
A49: r in {r} by TARSKI:def 1;
assume w in Y1 ; :: thesis: w in {r} + Y2
then consider k1 being Nat such that
A50: w = seq1 . k1 and
A51: n <= k1 by A45;
reconsider w1 = w as R_eal by A50;
A52: seq2 . k1 in Y2 by A47, A51;
w1 = r + (seq2 . k1) by A2, A50;
hence w in {r} + Y2 by A49, A52; :: thesis: verum
end;
then A53: Y1 c= {r} + Y2 by TARSKI:def 3;
now :: thesis: for w being object st w in {r} + Y2 holds
w in Y1
let w be object ; :: thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; :: thesis: w in Y1
then consider w1, w2 being R_eal such that
A54: w = w1 + w2 and
A55: w1 in {r} and
A56: w2 in Y2 ;
consider k2 being Nat such that
A57: w2 = seq2 . k2 and
A58: n <= k2 by A47, A56;
w1 = r by A55, TARSKI:def 1;
then w = seq1 . k2 by A2, A54, A57;
hence w in Y1 by A45, A58; :: thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A53, XBOOLE_0:def 10;
then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9;
then A59: inf Y1 = r + (inf Y2) by XXREAL_2:13;
A60: (inferior_realsequence seq2) . n in R2 by FUNCT_2:4;
r in {r} by TARSKI:def 1;
hence z in {r} + R2 by A46, A48, A59, A60; :: thesis: verum
end;
then R1 c= {r} + R2 by TARSKI:def 3;
then R1 = {r} + R2 by A22, XBOOLE_0:def 10;
then sup R1 = (sup {r}) + (sup R2) by A1, Th8;
hence lim_inf seq1 = r + (lim_inf seq2) by XXREAL_2:11; :: thesis: lim_sup seq1 = r + (lim_sup seq2)
now :: thesis: for z being object st z in P1 holds
z in {r} + P2
let z be object ; :: thesis: ( z in P1 implies z in {r} + P2 )
assume z in P1 ; :: thesis: z in {r} + P2
then consider n being object such that
A61: n in NAT and
A62: (superior_realsequence seq1) . n = z by FUNCT_2:11;
reconsider n = n as Element of NAT by A61;
consider Y1 being non empty Subset of ExtREAL such that
A63: Y1 = { (seq1 . k) where k is Nat : n <= k } and
A64: z = sup Y1 by A62, RINFSUP2:def 7;
consider Y2 being non empty Subset of ExtREAL such that
A65: Y2 = { (seq2 . k) where k is Nat : n <= k } and
A66: (superior_realsequence seq2) . n = sup Y2 by RINFSUP2:def 7;
now :: thesis: for w being object st w in Y1 holds
w in {r} + Y2
let w be object ; :: thesis: ( w in Y1 implies w in {r} + Y2 )
A67: r in {r} by TARSKI:def 1;
assume w in Y1 ; :: thesis: w in {r} + Y2
then consider k1 being Nat such that
A68: w = seq1 . k1 and
A69: n <= k1 by A63;
reconsider w1 = w as R_eal by A68;
A70: seq2 . k1 in Y2 by A65, A69;
w1 = r + (seq2 . k1) by A2, A68;
hence w in {r} + Y2 by A67, A70; :: thesis: verum
end;
then A71: Y1 c= {r} + Y2 by TARSKI:def 3;
now :: thesis: for w being object st w in {r} + Y2 holds
w in Y1
let w be object ; :: thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; :: thesis: w in Y1
then consider w1, w2 being R_eal such that
A72: w = w1 + w2 and
A73: w1 in {r} and
A74: w2 in Y2 ;
consider k2 being Nat such that
A75: w2 = seq2 . k2 and
A76: n <= k2 by A65, A74;
w1 = r by A73, TARSKI:def 1;
then w = seq1 . k2 by A2, A72, A75;
hence w in Y1 by A63, A76; :: thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A71, XBOOLE_0:def 10;
then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8;
then A77: sup Y1 = r + (sup Y2) by XXREAL_2:11;
A78: (superior_realsequence seq2) . n in P2 by FUNCT_2:4;
r in {r} by TARSKI:def 1;
hence z in {r} + P2 by A64, A66, A77, A78; :: thesis: verum
end;
then P1 c= {r} + P2 by TARSKI:def 3;
then P1 = {r} + P2 by A42, XBOOLE_0:def 10;
then inf P1 = (inf {r}) + (inf P2) by A1, Th9;
hence lim_sup seq1 = r + (lim_sup seq2) by XXREAL_2:13; :: thesis: verum