let seq be Real_Sequence; :: thesis: ( seq is non-increasing iff for n, k being Element of NAT holds seq . (n + k) <= seq . n )
thus ( seq is non-increasing implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) :: thesis: ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies seq is non-increasing )

proof

assume seq is non-increasing ; :: thesis: for n, k being Element of NAT holds seq . (n + k) <= seq . n
then for n being Element of NAT holds seq . (n + 1) <= seq . n by Lm9;
hence for n, k being Element of NAT holds seq . (n + k) <= seq . n by Lm5; :: thesis: verum

end;

assume for n, k being Element of NAT holds seq . (n + k) <= seq . n ; :: thesis: seq is non-increasing
then for n being Element of NAT holds seq . (n + 1) <= seq . n ;
hence seq is non-increasing by Lm9; :: thesis: verum