let f be Real_Sequence; :: thesis: ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
thus ( f is decreasing 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 decreasing )

proof

assume A1: f is decreasing ; :: 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)
( dom f = NAT & n < n + 1 ) by FUNCT_2:def 1, NAT_1:13;
hence f . n > f . (n + 1) by A1, Def2; :: thesis: verum

end;

assume A2: for n being Element of NAT holds f . n > f . (n + 1) ; :: thesis: f is decreasing
let m be Element of NAT ; :: according to SEQM_3:def 2 :: 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 that
m in dom f and
n in dom f and
A3: m < n ; :: thesis: f . m > f . n
ex k being Element of NAT st n = (m + 1) + k by A3, Lm1;
hence f . m > f . n by A2, Lm3; :: thesis: verum