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

assume that

A1: s is one-to-one and

A2: s is weakly-ascending ; :: thesis: s is ascending

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

s /. n <~ s /. m

assume that

A1: s is one-to-one and

A2: s is weakly-ascending ; :: thesis: s is ascending

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

s /. n <~ s /. m

proof

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

assume that

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

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

A5: s /. n <= s /. m by A3, A4, A2;

not s /. m <= s /. n

end;assume that

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

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

A5: s /. n <= s /. m by A3, A4, A2;

not s /. m <= s /. n

proof

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

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

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

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

hence contradiction by A3, A4, A1, FUNCT_1:def 4; :: thesis: verum

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

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

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

hence contradiction by A3, A4, A1, FUNCT_1:def 4; :: thesis: verum