let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for x being Element of X holds
( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
let F be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X holds
( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
let x be Element of X; :: thesis: ( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
A1: ( F # x is convergent_to_+infty implies - (F # x) is convergent_to_-infty ) by DBLSEQ_3:17;
( - (F # x) is convergent_to_-infty implies - (- (F # x)) is convergent_to_+infty ) by DBLSEQ_3:17;
hence A2: ( F # x is convergent_to_+infty iff (- F) # x is convergent_to_-infty ) by A1, DBLSEQ_3:2, Th38; :: thesis: ( ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
A3: ( F # x is convergent_to_-infty implies - (F # x) is convergent_to_+infty ) by DBLSEQ_3:17;
( - (F # x) is convergent_to_+infty implies - (- (F # x)) is convergent_to_-infty ) by DBLSEQ_3:17;
hence A4: ( F # x is convergent_to_-infty iff (- F) # x is convergent_to_+infty ) by A3, DBLSEQ_3:2, Th38; :: thesis: ( ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
A5: ( F # x is convergent_to_finite_number implies - (F # x) is convergent_to_finite_number ) by DBLSEQ_3:17;
( - (F # x) is convergent_to_finite_number implies - (- (F # x)) is convergent_to_finite_number ) by DBLSEQ_3:17;
hence A6: ( F # x is convergent_to_finite_number iff (- F) # x is convergent_to_finite_number ) by A5, Th38, DBLSEQ_3:2; :: thesis: ( ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
thus ( F # x is convergent iff (- F) # x is convergent ) by A2, A4, A6, MESFUNC5:def 11; :: thesis: ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) )

hereby :: thesis: verum

assume F # x is convergent ; :: thesis: lim ((- F) # x) = - (lim (F # x))
then lim (- (F # x)) = - (lim (F # x)) by DBLSEQ_3:17;
hence lim ((- F) # x) = - (lim (F # x)) by Th38; :: thesis: verum

end;