let f be Real_Sequence; :: thesis: ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
thus ( f is increasing implies for n being Element of NAT holds f . n < f . (n + 1) ) :: thesis: ( ( for n being Element of NAT holds f . n < f . (n + 1) ) implies f is increasing )

proof

assume A1: f is increasing ; :: thesis: for n being Element of NAT holds f . n < f . (n + 1)
let n be Element of NAT ; :: thesis: f . n < f . (n + 1)
A2: dom f = NAT by FUNCT_2:def 1;
n < n + 1 by NAT_1:13;
hence f . n < f . (n + 1) by A1, A2, Def1; :: thesis: verum

end;

assume A3: for n being Element of NAT holds f . n < f . (n + 1) ; :: thesis: f is increasing
let m be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n
let n be Element of NAT ; :: thesis: ( m in dom f & n in dom f & m < n implies f . m < f . n )
assume ( m in dom f & n in dom f & m < n ) ; :: thesis: f . m < f . n
then consider k being Element of NAT such that
A4: n = (m + 1) + k by Lm1;
thus f . m < f . n by A3, A4, Lm2; :: thesis: verum