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

let s be FinSequence of A; :: thesis: ( s is ascending iff Rev s is descending )
hereby :: thesis: ( Rev s is descending implies s is ascending )
assume A1: s is ascending ; :: thesis:
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 ;
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 ;
then A6: ( a in dom s & b in dom s ) by FINSEQ_1:def 3;
A7: s /. b = s . b by
.= (Rev s) . m by
.= (Rev s) /. m by ;
A8: s /. a = s . a by
.= (Rev s) . n by
.= (Rev s) /. n by ;
( a = ((len s) + 1) - n & b = ((len s) + 1) - m ) ;
then b < a by ;
then s /. b <~ s /. a by A1, A6;
hence (Rev s) /. m <~ (Rev s) /. n by A7, A8; :: thesis: verum
end;
hence Rev s is descending ; :: thesis: verum
end;
assume A9: Rev s is descending ; :: thesis: s is 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 ;
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 ;
then A14: ( a in dom s & b in dom s ) by ;
A15: s /. n = (Rev (Rev s)) . n by
.= (Rev s) . a by
.= (Rev s) /. a by ;
A16: s /. m = (Rev (Rev s)) . m by
.= (Rev s) . b by
.= (Rev s) /. b by ;
( a = ((len (Rev s)) + 1) - n & b = ((len (Rev s)) + 1) - m ) ;
then b < a by ;
hence s /. n <~ s /. m by A15, A16, A9, A13, A14; :: thesis: verum
end;
hence s is ascending ; :: thesis: verum