let s be FinSequence of A; :: thesis: ( s is weakly-ascending & s is weakly-descending implies s is constant )
assume A1: ( s is weakly-ascending & s is weakly-descending ) ; :: thesis: s is constant
for x, y being object st x in dom s & y in dom s holds
s . x = s . y
proof
let x, y be object ; :: thesis: ( x in dom s & y in dom s implies s . x = s . y )
assume A2: ( x in dom s & y in dom s ) ; :: thesis: s . x = s . y
then reconsider n = x, m = y as Nat ;
per cases ( n = m or n < m or m < n ) by XXREAL_0:1;
suppose n = m ; :: thesis: s . x = s . y
hence s . x = s . y ; :: thesis: verum
end;
suppose n < m ; :: thesis: s . x = s . y
then ( s /. n <= s /. m & s /. m <= s /. n ) by A1, A2;
then A3: ( [(s /. n),(s /. m)] in the InternalRel of A & [(s /. m),(s /. n)] in the InternalRel of A ) by ORDERS_2:def 5;
A4: ( s . x = s /. n & s . y = s /. m ) by A2, PARTFUN1:def 6;
( s . x in the carrier of A & s . y in the carrier of A ) by A2, PARTFUN1:4;
hence s . x = s . y by A3, A4, ORDERS_2:def 4, RELAT_2:def 4; :: thesis: verum
end;
suppose m < n ; :: thesis: s . x = s . y
then ( s /. n <= s /. m & s /. m <= s /. n ) by A1, A2;
then A5: ( [(s /. n),(s /. m)] in the InternalRel of A & [(s /. m),(s /. n)] in the InternalRel of A ) by ORDERS_2:def 5;
A6: ( s . x = s /. n & s . y = s /. m ) by A2, PARTFUN1:def 6;
( s . x in the carrier of A & s . y in the carrier of A ) by A2, PARTFUN1:4;
hence s . x = s . y by A5, A6, ORDERS_2:def 4, RELAT_2:def 4; :: thesis: verum
end;
end;
end;
hence s is constant by FUNCT_1:def 10; :: thesis: verum