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

A2: now

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

end;

incl NAT is divergent_to+infty by Lm4, Th47;
then (- 1) (#) (incl NAT) is divergent_to-infty by Th40;
hence seq is divergent_to-infty by A2, FUNCT_2:63; :: thesis: verum