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

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

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

s /. m <~ s /. n ;

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

s /. m <= s /. n

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

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

s /. m <~ s /. n ;

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 weakly-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

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

A3: n < m ; :: thesis: s /. m <= s /. n

s /. m <~ s /. n by A1, A2, A3;

hence s /. m <= s /. n ; :: thesis: verum

end;assume that

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

A3: n < m ; :: thesis: s /. m <= s /. n

s /. m <~ s /. n by A1, A2, A3;

hence s /. m <= s /. n ; :: thesis: verum