let seq be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Nat holds seq . n <= 0 ) implies lim seq <= 0 )

assume that

A1: seq is convergent and

A2: for n being Nat holds seq . n <= 0 ; :: thesis: lim seq <= 0

set seq1 = - seq;

then 0 <= lim (- seq) by A3, SEQ_2:17;

then - 0 <= - (lim seq) by A1, SEQ_2:10;

hence lim seq <= 0 by XREAL_1:24; :: thesis: verum

assume that

A1: seq is convergent and

A2: for n being Nat holds seq . n <= 0 ; :: thesis: lim seq <= 0

set seq1 = - seq;

A3: now :: thesis: for n being Nat holds - 0 <= (- seq) . n

- seq is convergent
by A1, SEQ_2:9;let n be Nat; :: thesis: - 0 <= (- seq) . n

( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:10;

hence - 0 <= (- seq) . n by XREAL_1:24; :: thesis: verum

end;( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:10;

hence - 0 <= (- seq) . n by XREAL_1:24; :: thesis: verum

then 0 <= lim (- seq) by A3, SEQ_2:17;

then - 0 <= - (lim seq) by A1, SEQ_2:10;

hence lim seq <= 0 by XREAL_1:24; :: thesis: verum