let A be RelStr ; :: thesis: for s being FinSequence of A holds
( s is weakly-ascending iff Rev s is weakly-descending )
let s be FinSequence of A; :: thesis: ( s is weakly-ascending iff Rev s is weakly-descending )

hereby :: thesis: ( Rev s is weakly-descending implies s is weakly-ascending )

assume A1: s is weakly-ascending ; :: thesis: Rev s is weakly-descending

now :: thesis: for n, m being Nat st n in dom (Rev s) & m in dom (Rev s) & n < m holds
(Rev s) /. m <= (Rev s) /. n

let n, m be Nat; :: thesis: ( n in dom (Rev s) & m in dom (Rev s) & n < m implies (Rev s) /. m <= (Rev s) /. n )
assume that
A2: ( n in dom (Rev s) & m in dom (Rev s) ) and
A3: n < m ; :: thesis: (Rev s) /. m <= (Rev s) /. n
set l = len s;
A4: ( n in dom s & m in dom s ) by A2, FINSEQ_5:57;
then A5: ( n in Seg (len s) & m in Seg (len s) ) by FINSEQ_1:def 3;
then ( n <= len s & m <= len s ) by FINSEQ_1:1;
then reconsider a = ((len s) - n) + 1, b = ((len s) - m) + 1 as Nat by FINSEQ_5:1;
( a in Seg (len s) & b in Seg (len s) ) by A5, FINSEQ_5:2;
then A6: ( a in dom s & b in dom s ) by FINSEQ_1:def 3;
A7: s /. b = s . b by A6, PARTFUN1:def 6
.= (Rev s) . m by A4, FINSEQ_5:58
.= (Rev s) /. m by A2, PARTFUN1:def 6 ;
A8: s /. a = s . a by A6, PARTFUN1:def 6
.= (Rev s) . n by A4, FINSEQ_5:58
.= (Rev s) /. n by A2, PARTFUN1:def 6 ;
( a = ((len s) + 1) - n & b = ((len s) + 1) - m ) ;
then b < a by A3, XREAL_1:15;
hence (Rev s) /. m <= (Rev s) /. n by A7, A8, A1, A6; :: thesis: verum

end;

hence Rev s is weakly-descending ; :: thesis: verum

end;

assume A9: Rev s is weakly-descending ; :: thesis: s is weakly-ascending

now :: thesis: for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <= s /. m

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. n <= s /. m )
assume that
A10: ( n in dom s & m in dom s ) and
A11: n < m ; :: thesis: s /. n <= s /. m
set l = len (Rev s);
( n in dom (Rev s) & m in dom (Rev s) ) by A10, FINSEQ_5:57;
then A12: ( n in Seg (len (Rev s)) & m in Seg (len (Rev s)) ) by FINSEQ_1:def 3;
then ( n <= len (Rev s) & m <= len (Rev s) ) by FINSEQ_1:1;
then reconsider a = ((len (Rev s)) - n) + 1, b = ((len (Rev s)) - m) + 1 as Nat by FINSEQ_5:1;
A13: dom s = dom (Rev s) by FINSEQ_5:57;
( a in Seg (len (Rev s)) & b in Seg (len (Rev s)) ) by A12, FINSEQ_5:2;
then A14: ( a in dom s & b in dom s ) by A13, FINSEQ_1:def 3;
A15: s /. n = (Rev (Rev s)) . n by A10, PARTFUN1:def 6
.= (Rev s) . a by A13, A10, FINSEQ_5:58
.= (Rev s) /. a by A14, A13, PARTFUN1:def 6 ;
A16: s /. m = (Rev (Rev s)) . m by A10, PARTFUN1:def 6
.= (Rev s) . b by A13, A10, FINSEQ_5:58
.= (Rev s) /. b by A14, A13, PARTFUN1:def 6 ;
( a = ((len (Rev s)) + 1) - n & b = ((len (Rev s)) + 1) - m ) ;
then b < a by A11, XREAL_1:15;
hence s /. n <= s /. m by A15, A16, A9, A13, A14; :: thesis: verum

end;

hence s is weakly-ascending ; :: thesis: verum