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 )

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

hence
( s is weakly-ascending & s is weakly-descending )
; :: thesis: verum
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;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