let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n = - n ) implies seq is divergent_to-infty )
assume A1: for n being Nat holds seq . n = - n ; :: thesis: seq is divergent_to-infty

A2: now :: thesis: for n being Element of NAT holds (- s1) . n = seq . n

let n be Element of NAT ; :: thesis: (- s1) . n = seq . n
thus (- s1) . n = - (s1 . n) by SEQ_1:10
.= - n
.= seq . n by A1 ; :: thesis: verum

end;

s1 is divergent_to+infty by Lm5, Th20;
then (- jj) (#) s1 is divergent_to-infty by Th13;
hence seq is divergent_to-infty by A2, FUNCT_2:63; :: thesis: verum