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 & 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 & 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 & 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
A1: dom (F1 . 0) = dom (F2 . 0) and
A2: F1 is with_the_same_dom and
A3: f " {+infty} = {} and
A4: f " {-infty} = {} and
A5: 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) )
A6: F1 . 0 = f + (F2 . 0) by A5;
A7: dom (f + (F2 . 0)) = ((dom f) /\ (dom (F2 . 0))) \ (((f " {-infty}) /\ ((F2 . 0) " {+infty})) \/ ((f " {+infty}) /\ ((F2 . 0) " {-infty}))) by MESFUNC1:def 3;
A8: 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 A9: dom (f + (lim_sup F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def 8;
then A10: dom (lim_sup F1) = dom (f + (lim_sup F2)) by A3, A4, A6, A7, MESFUNC8:def 8;
A11: 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 A12: dom (f + (lim_inf F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def 7;
then A13: dom (lim_inf F1) = dom (f + (lim_inf F2)) by A3, A4, A6, A7, MESFUNC8:def 7;
A14: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def 7;
A15: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def 7;
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 A16: x in dom (lim_inf F1) ; :: thesis: (lim_inf F1) . x = (f + (lim_inf F2)) . x
then A17: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def 7;
A18: 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 A5;
then dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def 2;
then A19: x in dom (f + (F2 . n)) by A16, MESFUNC8:def 7;
(F1 . n) . x = (f + (F2 . n)) . x by A5;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A19, 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;

A20: dom (f + (lim_inf F2)) c= dom f by A3, A4, A11, XBOOLE_1:17;
then not f . x in {-infty} by A4, A13, A16, FUNCT_1:def 7;
then A21: f . x <> -infty by TARSKI:def 1;
not f . x in {+infty} by A3, A13, A16, A20, FUNCT_1:def 7;
then f . x <> +infty by TARSKI:def 1;
then A22: f . x in REAL by A21, XXREAL_0:14;
x in dom (f + (lim_inf F2)) by A3, A4, A6, A7, A12, A16, MESFUNC8:def 7;
then A23: (f + (lim_inf F2)) . x = (f . x) + ((lim_inf F2) . x) by MESFUNC1:def 3;
(lim_inf F2) . x = lim_inf (F2 # x) by A1, A15, A14, A16, MESFUNC8:def 7;
hence (lim_inf F1) . x = (f + (lim_inf F2)) . x by A22, A18, A17, A23, Th10; :: thesis: verum

end;

hence lim_inf F1 = f + (lim_inf F2) by A13, PARTFUN1:5; :: thesis: lim_sup F1 = f + (lim_sup F2)
A24: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def 8;
A25: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def 8;
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 A26: x in dom (lim_sup F1) ; :: thesis: (lim_sup F1) . x = (f + (lim_sup F2)) . x
then A27: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def 8;
A28: 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 A5;
then A29: dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def 2;
(F1 . n) . x = (f + (F2 . n)) . x by A5;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A24, A26, A29, 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;

A30: dom (f + (lim_sup F2)) c= dom f by A3, A4, A8, XBOOLE_1:17;
then not f . x in {-infty} by A4, A10, A26, FUNCT_1:def 7;
then A31: f . x <> -infty by TARSKI:def 1;
not f . x in {+infty} by A3, A10, A26, A30, FUNCT_1:def 7;
then f . x <> +infty by TARSKI:def 1;
then A32: f . x in REAL by A31, XXREAL_0:14;
x in dom (f + (lim_sup F2)) by A3, A4, A6, A7, A9, A26, MESFUNC8:def 8;
then A33: (f + (lim_sup F2)) . x = (f . x) + ((lim_sup F2) . x) by MESFUNC1:def 3;
(lim_sup F2) . x = lim_sup (F2 # x) by A1, A24, A25, A26, MESFUNC8:def 8;
hence (lim_sup F1) . x = (f + (lim_sup F2)) . x by A32, A28, A27, A33, Th10; :: thesis: verum

end;

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