let s be FinSequence of A; :: thesis: ( s is ascending implies s is asc_ordering )
assume A1: s is ascending ; :: thesis: s is asc_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
A2: ( x in dom s & y in dom s ) and
A3: s . x = s . y ; :: thesis: x = y
reconsider n = x, m = y as Nat by A2;
( s . x = s /. n & s . y = s /. m ) by A2, PARTFUN1:def 6;
then A4: s /. n = s /. m by A3;
per cases ( n < m or n = m or m < n ) by XXREAL_0:1;
suppose n < m ; :: thesis: x = y
hence x = y by A4, A2, A1; :: thesis: verum
end;
suppose n = m ; :: thesis: x = y
hence x = y ; :: thesis: verum
end;
suppose m < n ; :: thesis: x = y
then s /. m <~ s /. n by A2, A1;
hence x = y by A4; :: thesis: verum
end;
end;
end;
hence s is asc_ordering by A1, FUNCT_1:def 4; :: thesis: verum