let R be real-valued FinSequence; :: thesis: ( R is non-increasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n >= R . m )
thus ( R is non-increasing implies for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n >= R . m ) ; :: thesis: ( ( for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n >= R . m ) implies R is non-increasing )
assume A1: for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n >= R . m ; :: thesis: R is non-increasing
let n be Nat; :: according to RFINSEQ:def 3 :: thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) )
n < n + 1 by NAT_1:13;
hence ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) ) by A1; :: thesis: verum