let s be FinSequence of A; :: thesis: ( s is descending implies s is desc_ordering )
assume A5: s is descending ; :: thesis: s is desc_ordering
for x, y being object st x in dom s & y in dom s & s . x = s . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom s & y in dom s & s . x = s . y implies x = y )
assume that
A6: ( x in dom s & y in dom s ) and
A7: s . x = s . y ; :: thesis: x = y
reconsider n = x, m = y as Nat by A6;
( s . x = s /. n & s . y = s /. m ) by A6, PARTFUN1:def 6;
then A8: s /. n = s /. m by A7;

per cases ( n < m or n = m or m < n ) by XXREAL_0:1;

suppose n < m ; :: thesis: x = y

hence x = y by A8, A6, A5; :: thesis: verum

end;

suppose n = m ; :: thesis: x = y

hence x = y ; :: thesis: verum

end;

suppose m < n ; :: thesis: x = y

then s /. n <~ s /. m by A6, A5;
hence x = y by A8; :: thesis: verum

end;

end;

end;

hence s is desc_ordering by A5, FUNCT_1:def 4; :: thesis: verum