let seq be Real_Sequence; :: thesis: ( seq is V95() iff - seq is V96() )
set seq1 = - seq;
thus ( seq is V95() implies - seq is V96() ) ; :: thesis: ( - seq is V96() implies seq is V95() )
assume - seq is V96() ; :: thesis: seq is V95()
then consider t being Real such that
A1: for n being Nat holds (- seq) . n > t by SEQ_2:def 4;
for n being Nat holds seq . n < - t

proof

let n be Nat; :: thesis: seq . n < - t
(- seq) . n = - (seq . n) by SEQ_1:10;
then A2: - ((- seq) . n) = seq . n ;
(- seq) . n > t by A1;
hence seq . n < - t by A2, XREAL_1:24; :: thesis: verum

end;

hence seq is V95() by SEQ_2:def 3; :: thesis: verum