let seq be Real_Sequence; :: thesis: ( seq is V88() iff - seq is V89() )
set seq1 = - seq;
thus ( seq is V88() implies - seq is V89() ) ; :: thesis: ( - seq is V89() implies seq is V88() )
assume - seq is V89() ; :: thesis: seq is V88()
then consider t being real number such that
A1: for n being Element of NAT holds (- seq) . n > t by SEQ_2:def 4;
for n being Element of NAT holds seq . n < - t

proof

let n be Element of 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 V88() by SEQ_2:def 3; :: thesis: verum