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 & F2 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 & F2 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 ) & F1 is with_the_same_dom & F2 is with_the_same_dom ) and
A2: for n being Nat holds F1 . n = - (F2 . n) ; :: thesis: ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
A3: ( dom (lim_inf F1) = dom (F1 . 0 ) & dom (lim_sup F2) = dom (F2 . 0 ) & dom (lim_sup F1) = dom (F1 . 0 ) & dom (lim_inf F2) = dom (F2 . 0 ) ) by MESFUNC8:def 8, MESFUNC8:def 9;
A5: dom (- (lim_sup F2)) = dom (lim_sup F2) by MESFUNC1:def 7;

A6: now

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 A61: 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 A1, MESFUNC8:def 2;
then A62: x in dom (- (F2 . n)) by A61, A2;
(F1 . n) . x = (- (F2 . n)) . x by A2;
then (F1 . n) . x = - ((F2 . n) . x) by A62, 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;

now

let x be Element of X; :: thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (- (lim_sup F2)) . x )
assume P01: x in dom (lim_inf F1) ; :: thesis: (lim_inf F1) . x = (- (lim_sup F2)) . x
then P07: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A3, A6;
P08: ( (lim_inf F1) . x = lim_inf (F1 # x) & (lim_sup F2) . x = lim_sup (F2 # x) ) by P01, A3, A1, MESFUNC8:def 8, MESFUNC8:def 9;
x in dom (- (lim_sup F2)) by P01, A3, A1, MESFUNC1:def 7;
then (- (lim_sup F2)) . x = - ((lim_sup F2) . x) by MESFUNC1:def 7;
hence (lim_inf F1) . x = (- (lim_sup F2)) . x by P08, P07, supinfa; :: thesis: verum

end;

hence lim_inf F1 = - (lim_sup F2) by A5, A3, A1, PARTFUN1:34; :: thesis: lim_sup F1 = - (lim_inf F2)
B5: dom (- (lim_inf F2)) = dom (lim_inf F2) by MESFUNC1:def 7;
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 Q01: x in dom (lim_sup F1) ; :: thesis: (lim_sup F1) . x = (- (lim_inf F2)) . x
then Q07: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A3, A6;
Q08: ( (lim_sup F1) . x = lim_sup (F1 # x) & (lim_inf F2) . x = lim_inf (F2 # x) ) by Q01, A1, A3, MESFUNC8:def 8, MESFUNC8:def 9;
x in dom (- (lim_inf F2)) by Q01, A1, A3, MESFUNC1:def 7;
then (- (lim_inf F2)) . x = - ((lim_inf F2) . x) by MESFUNC1:def 7;
hence (lim_sup F1) . x = (- (lim_inf F2)) . x by Q08, Q07, supinfa; :: thesis: verum

end;

hence lim_sup F1 = - (lim_inf F2) by A1, A3, B5, PARTFUN1:34; :: thesis: verum