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

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

hence
s is asc_ordering
by A1, FUNCT_1:def 4; :: thesis: verum
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;

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