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
incl NAT is divergent_to+infty by Lm7, Th47;
then A2: (- 1) (#) (incl NAT ) is divergent_to-infty by Th40;

now

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

end;

hence seq is divergent_to-infty by A2, FUNCT_2:113; :: thesis: verum