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

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