for a being FinSequence holds
( a is ascending iff for n, m being Nat st n <= m & n in dom a & m in dom a holds
a . n c= a . m )