let X be non empty set ; :: thesis: for F1, F2 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st dom (F1 . 0 ) = dom (F2 . 0 ) & F1 is with_the_same_dom & F2 is with_the_same_dom & f " {+infty } = {} & f " {-infty } = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
let F1, F2 be Functional_Sequence of X,ExtREAL ; :: thesis: for f being PartFunc of X,ExtREAL st dom (F1 . 0 ) = dom (F2 . 0 ) & F1 is with_the_same_dom & F2 is with_the_same_dom & f " {+infty } = {} & f " {-infty } = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
let f be PartFunc of X,ExtREAL ; :: thesis: ( dom (F1 . 0 ) = dom (F2 . 0 ) & F1 is with_the_same_dom & F2 is with_the_same_dom & f " {+infty } = {} & f " {-infty } = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) implies ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) )
assume that
A0: ( dom (F1 . 0 ) = dom (F2 . 0 ) & F1 is with_the_same_dom & F2 is with_the_same_dom ) and
A1: ( f " {+infty } = {} & f " {-infty } = {} ) and
A2: for n being Nat holds F1 . n = f + (F2 . n) ; :: thesis: ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
A3: F1 . 0 = f + (F2 . 0 ) by A2;
A4: dom (f + (F2 . 0 )) = ((dom f) /\ (dom (F2 . 0 ))) \ (((f " {-infty }) /\ ((F2 . 0 ) " {+infty })) \/ ((f " {+infty }) /\ ((F2 . 0 ) " {-infty }))) by MESFUNC1:def 3;
A5: ( dom (lim_inf F1) = dom (F1 . 0 ) & dom (lim_inf F2) = dom (F2 . 0 ) ) by MESFUNC8:def 8;
A6: dom (f + (lim_inf F2)) = ((dom f) /\ (dom (lim_inf F2))) \ (((f " {-infty }) /\ ((lim_inf F2) " {+infty })) \/ ((f " {+infty }) /\ ((lim_inf F2) " {-infty }))) by MESFUNC1:def 3;
then Z7: dom (f + (lim_inf F2)) = (dom f) /\ (dom (F2 . 0 )) by A1, MESFUNC8:def 8;
then A7: dom (lim_inf F1) = dom (f + (lim_inf F2)) by A3, A4, A1, MESFUNC8:def 8;
for x being Element of X st x in dom (lim_inf F1) holds
(lim_inf F1) . x = (f + (lim_inf F2)) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (f + (lim_inf F2)) . x )
assume P01: x in dom (lim_inf F1) ; :: thesis: (lim_inf F1) . x = (f + (lim_inf F2)) . x
R02: dom (f + (lim_inf F2)) c= dom f by A6, A1, XBOOLE_1:17;
then not f . x in {+infty } by A1, P01, A7, FUNCT_1:def 13;
then R04: f . x <> +infty by TARSKI:def 1;
not f . x in {-infty } by A1, R02, P01, A7, FUNCT_1:def 13;
then f . x <> -infty by TARSKI:def 1;
then RR: f . x is Real by R04, XXREAL_0:14;
P07: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n)

proof

let n be Nat; :: thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n)
F1 . n = f + (F2 . n) by A2;
then dom (f + (F2 . n)) = dom (F1 . 0 ) by A0, MESFUNC8:def 2;
then P06: x in dom (f + (F2 . n)) by P01, MESFUNC8:def 8;
(F1 . n) . x = (f + (F2 . n)) . x by A2;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by P06, MESFUNC1:def 3;
then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def 13;
hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def 13; :: thesis: verum

end;

P08: ( (lim_inf F1) . x = lim_inf (F1 # x) & (lim_inf F2) . x = lim_inf (F2 # x) ) by P01, A5, A0, MESFUNC8:def 8;
x in dom (f + (lim_inf F2)) by P01, Z7, A4, A1, A3, MESFUNC8:def 8;
then (f + (lim_inf F2)) . x = (f . x) + ((lim_inf F2) . x) by MESFUNC1:def 3;
hence (lim_inf F1) . x = (f + (lim_inf F2)) . x by P07, P08, RR, limseq2; :: thesis: verum

end;

hence lim_inf F1 = f + (lim_inf F2) by A7, PARTFUN1:34; :: thesis: lim_sup F1 = f + (lim_sup F2)
B5: ( dom (lim_sup F1) = dom (F1 . 0 ) & dom (lim_sup F2) = dom (F2 . 0 ) ) by MESFUNC8:def 9;
BB: dom (f + (lim_sup F2)) = ((dom f) /\ (dom (lim_sup F2))) \ (((f " {-infty }) /\ ((lim_sup F2) " {+infty })) \/ ((f " {+infty }) /\ ((lim_sup F2) " {-infty }))) by MESFUNC1:def 3;
then B6: dom (f + (lim_sup F2)) = (dom f) /\ (dom (F2 . 0 )) by A1, MESFUNC8:def 9;
then B7: dom (lim_sup F1) = dom (f + (lim_sup F2)) by A3, A4, A1, MESFUNC8:def 9;
for x being Element of X st x in dom (lim_sup F1) holds
(lim_sup F1) . x = (f + (lim_sup F2)) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (f + (lim_sup F2)) . x )
assume Q01: x in dom (lim_sup F1) ; :: thesis: (lim_sup F1) . x = (f + (lim_sup F2)) . x
R02: dom (f + (lim_sup F2)) c= dom f by A1, BB, XBOOLE_1:17;
then not f . x in {+infty } by A1, B7, Q01, FUNCT_1:def 13;
then R04: f . x <> +infty by TARSKI:def 1;
not f . x in {-infty } by A1, B7, Q01, R02, FUNCT_1:def 13;
then f . x <> -infty by TARSKI:def 1;
then RR: f . x is Real by R04, XXREAL_0:14;
Q07: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n)

proof

let n be Nat; :: thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n)
F1 . n = f + (F2 . n) by A2;
then Q06: dom (f + (F2 . n)) = dom (F1 . 0 ) by A0, MESFUNC8:def 2;
(F1 . n) . x = (f + (F2 . n)) . x by A2;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by Q06, Q01, B5, MESFUNC1:def 3;
then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def 13;
hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def 13; :: thesis: verum

end;

Q08: ( (lim_sup F1) . x = lim_sup (F1 # x) & (lim_sup F2) . x = lim_sup (F2 # x) ) by Q01, B5, A0, MESFUNC8:def 9;
x in dom (f + (lim_sup F2)) by Q01, B6, A4, A1, A3, MESFUNC8:def 9;
then (f + (lim_sup F2)) . x = (f . x) + ((lim_sup F2) . x) by MESFUNC1:def 3;
hence (lim_sup F1) . x = (f + (lim_sup F2)) . x by Q07, Q08, RR, limseq2; :: thesis: verum

end;

hence lim_sup F1 = f + (lim_sup F2) by B7, PARTFUN1:34; :: thesis: verum