let s be FinSequence of A; :: thesis: ( s is ascending implies s is weakly-ascending )
assume s is ascending ; :: thesis: s is weakly-ascending
then A1: for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <~ s /. m ;
for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <= s /. m
proof
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. n <= s /. m )
assume that
A2: ( n in dom s & m in dom s ) and
A3: n < m ; :: thesis: s /. n <= s /. m
s /. n <~ s /. m by A1, A2, A3;
hence s /. n <= s /. m ; :: thesis: verum
end;
hence s is weakly-ascending ; :: thesis: verum