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

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

hence
s is desc_ordering
by A5, 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

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;

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