let f be FinSequence; :: thesis: ( f is weakly-one-to-one implies Rev f is weakly-one-to-one )
assume A1: f is weakly-one-to-one ; :: thesis: Rev f is weakly-one-to-one
A2: len f = len (Rev f) by FINSEQ_5:def 3;
let i be Nat; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len (Rev f) implies (Rev f) . i <> (Rev f) . (i + 1) )
assume that
A3: 1 <= i and
A4: i < len (Rev f) ; :: thesis: (Rev f) . i <> (Rev f) . (i + 1)
A5: i + 1 <= len (Rev f) by A4, NAT_1:13;
i + 1 >= 1 by NAT_1:11;
then A6: i + 1 in Seg (len (Rev f)) by A5, FINSEQ_1:1;
then i + 1 in dom (Rev f) by FINSEQ_1:def 3;
then A7: (Rev f) . (i + 1) = f . (((len f) - (i + 1)) + 1) by FINSEQ_5:def 3;
A8: i in Seg (len (Rev f)) by A3, A4, FINSEQ_1:1;
then i in dom (Rev f) by FINSEQ_1:def 3;
then A9: (Rev f) . i = f . (((len f) - i) + 1) by FINSEQ_5:def 3;
((len f) - (i + 1)) + 1 = (len f) - i ;
then reconsider j = (len f) - i as Nat by A2, A5, FINSEQ_5:1;
((len f) - i) + 1 in Seg (len f) by A2, A8, FINSEQ_5:2;
then j + 1 <= len f by FINSEQ_1:1;
then A10: j < len f by NAT_1:13;
((len f) - (i + 1)) + 1 in Seg (len f) by A2, A6, FINSEQ_5:2;
then j >= 1 by FINSEQ_1:1;
hence (Rev f) . i <> (Rev f) . (i + 1) by A1, A9, A7, A10; :: thesis: verum