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
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < seq . m
consider n being Nat such that
A2: r < n by SEQ_4:3;
take n ; :: thesis: for m being Nat st n <= m holds
r < seq . m
let m be Nat; :: thesis: ( n <= m implies r < seq . m )
assume n <= m ; :: thesis: r < seq . m
then r < m by A2, XXREAL_0:2;
hence r < seq . m by A1; :: thesis: verum