let f be sequence of NAT ; :: thesis: ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
reconsider f = f as Real_Sequence by FUNCT_2:9;
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) by Lm6;
hence ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) ; :: thesis: verum