let X be non empty set ; :: thesis: for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds
( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
let F1, F2 be Functional_Sequence of X,ExtREAL; :: thesis: ( dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) implies ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) )
assume that
A1: dom (F1 . 0) = dom (F2 . 0) and
A2: F1 is with_the_same_dom and
A3: for n being Nat holds F1 . n = - (F2 . n) ; :: thesis: ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
A4: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def 7;
A5: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def 8;

A6: now :: thesis: for x being Element of X st x in dom (F1 . 0) holds
for n being Nat holds (F2 # x) . n = - ((F1 # x) . n)

let x be Element of X; :: thesis: ( x in dom (F1 . 0) implies for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) )
assume A7: x in dom (F1 . 0) ; :: thesis: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n)
let n be Nat; :: thesis: (F2 # x) . n = - ((F1 # x) . n)
dom (F1 . n) = dom (F1 . 0) by A2, MESFUNC8:def 2;
then A8: x in dom (- (F2 . n)) by A3, A7;
(F1 . n) . x = (- (F2 . n)) . x by A3;
then (F1 . n) . x = - ((F2 . n) . x) by A8, MESFUNC1:def 7;
then (F1 # x) . n = - ((F2 . n) . x) by MESFUNC5:def 13;
hence (F2 # x) . n = - ((F1 # x) . n) by MESFUNC5:def 13; :: thesis: verum

end;

A9: now :: thesis: for x being Element of X st x in dom (lim_inf F1) holds
(lim_inf F1) . x = (- (lim_sup F2)) . x

let x be Element of X; :: thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (- (lim_sup F2)) . x )
assume A10: x in dom (lim_inf F1) ; :: thesis: (lim_inf F1) . x = (- (lim_sup F2)) . x
then A11: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def 7;
x in dom (- (lim_sup F2)) by A1, A4, A5, A10, MESFUNC1:def 7;
then A12: (- (lim_sup F2)) . x = - ((lim_sup F2) . x) by MESFUNC1:def 7;
A13: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A4, A6, A10;
(lim_sup F2) . x = lim_sup (F2 # x) by A1, A4, A5, A10, MESFUNC8:def 8;
hence (lim_inf F1) . x = (- (lim_sup F2)) . x by A13, A11, A12, Th14; :: thesis: verum

end;

dom (- (lim_sup F2)) = dom (lim_sup F2) by MESFUNC1:def 7;
hence lim_inf F1 = - (lim_sup F2) by A1, A4, A5, A9, PARTFUN1:5; :: thesis: lim_sup F1 = - (lim_inf F2)
A14: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def 8;
A15: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def 7;
A16: for x being Element of X st x in dom (lim_sup F1) holds
(lim_sup F1) . x = (- (lim_inf F2)) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (- (lim_inf F2)) . x )
assume A17: x in dom (lim_sup F1) ; :: thesis: (lim_sup F1) . x = (- (lim_inf F2)) . x
then A18: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def 8;
x in dom (- (lim_inf F2)) by A1, A14, A15, A17, MESFUNC1:def 7;
then A19: (- (lim_inf F2)) . x = - ((lim_inf F2) . x) by MESFUNC1:def 7;
A20: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A14, A6, A17;
(lim_inf F2) . x = lim_inf (F2 # x) by A1, A14, A15, A17, MESFUNC8:def 7;
hence (lim_sup F1) . x = (- (lim_inf F2)) . x by A20, A18, A19, Th14; :: thesis: verum

end;

dom (- (lim_inf F2)) = dom (lim_inf F2) by MESFUNC1:def 7;
hence lim_sup F1 = - (lim_inf F2) by A1, A14, A15, A16, PARTFUN1:5; :: thesis: verum