:: deftheorem defines decreasing SEQM_3:def 2 :
for f being NAT -defined real-valued Function holds
( f is decreasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds
f . m > f . n );