let X be non empty set ; 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; 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; ( 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)
; ( 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;
( x in dom (lim_inf F1) implies (lim_inf F1) . x = (f + (lim_inf F2)) . x )
assume A16:
x in dom (lim_inf F1)
;
(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)
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;
verum
end;
hence
lim_inf F1 = f + (lim_inf F2)
by A13, PARTFUN1:5; 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;
( x in dom (lim_sup F1) implies (lim_sup F1) . x = (f + (lim_sup F2)) . x )
assume A26:
x in dom (lim_sup F1)
;
(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)
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;
verum
end;
hence
lim_sup F1 = f + (lim_sup F2)
by A10, PARTFUN1:5; verum