let s be FinSequence of A; :: thesis: ( s is one-to-one & s is weakly-descending implies s is descending )

assume that

A6: s is one-to-one and

A7: s is weakly-descending ; :: thesis: s is descending

for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. m <~ s /. n

assume that

A6: s is one-to-one and

A7: s is weakly-descending ; :: thesis: s is descending

for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. m <~ s /. n

proof

hence
s is descending
; :: thesis: verum
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. m <~ s /. n )

assume that

A8: ( n in dom s & m in dom s ) and

A9: n < m ; :: thesis: s /. m <~ s /. n

A10: s /. m <= s /. n by A8, A9, A7;

not s /. n <= s /. m

end;assume that

A8: ( n in dom s & m in dom s ) and

A9: n < m ; :: thesis: s /. m <~ s /. n

A10: s /. m <= s /. n by A8, A9, A7;

not s /. n <= s /. m

proof

hence
s /. m <~ s /. n
by A10; :: thesis: verum
assume
s /. n <= s /. m
; :: thesis: contradiction

then s /. m = s /. n by A10, ORDERS_2:2;

then s . m = s /. n by A8, PARTFUN1:def 6;

then s . m = s . n by A8, PARTFUN1:def 6;

hence contradiction by A8, A9, A6, FUNCT_1:def 4; :: thesis: verum

end;then s /. m = s /. n by A10, ORDERS_2:2;

then s . m = s /. n by A8, PARTFUN1:def 6;

then s . m = s . n by A8, PARTFUN1:def 6;

hence contradiction by A8, A9, A6, FUNCT_1:def 4; :: thesis: verum