let s be FinSequence of A; :: thesis: ( s is constant implies ( s is weakly-ascending & s is weakly-descending ) )
assume A1: s is constant ; :: thesis: ( s is weakly-ascending & s is weakly-descending )
for n, m being Nat st n in dom s & m in dom s & n < m holds
( s /. n <= s /. m & s /. m <= s /. n )

proof

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies ( s /. n <= s /. m & s /. m <= s /. n ) )
assume A2: ( n in dom s & m in dom s & n < m ) ; :: thesis: ( s /. n <= s /. m & s /. m <= s /. n )
then A3: s . n = s . m by A1, FUNCT_1:def 10;
A4: ( s . n = s /. n & s . m = s /. m ) by A2, PARTFUN1:def 6;
s . n in the carrier of A by A2, PARTFUN1:4;
then [(s . n),(s . n)] in the InternalRel of A by RELAT_2:def 1, ORDERS_2:def 2;
hence ( s /. n <= s /. m & s /. m <= s /. n ) by A3, A4, ORDERS_2:def 5; :: thesis: verum

end;

hence ( s is weakly-ascending & s is weakly-descending ) ; :: thesis: verum