let R be FinSequence of REAL ; :: 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) )
A2: n < n + 1 by NAT_1:13;
assume ( n in dom R & n + 1 in dom R ) ; :: thesis: R . n >= R . (n + 1)
hence R . n >= R . (n + 1) by A1, A2; :: thesis: verum