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

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

hence
s is constant
by FUNCT_1:def 10; :: thesis: verum
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 ;

end;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;

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;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

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;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