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
let i be Element of NAT ; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len (Rev f) implies (Rev f) . i <> (Rev f) . (i + 1) )
assume that
A2: 1 <= i and
A3: i < len (Rev f) ; :: thesis: (Rev f) . i <> (Rev f) . (i + 1)
A4: len f = len (Rev f) by FINSEQ_5:def 3;
A5: i in Seg (len (Rev f)) by A2, A3, FINSEQ_1:3;
then A6: i in dom (Rev f) by FINSEQ_1:def 3;
A7: i + 1 >= 1 by NAT_1:11;
A8: i + 1 <= len (Rev f) by A3, NAT_1:13;
then A9: i + 1 in Seg (len (Rev f)) by A7, FINSEQ_1:3;
then i + 1 in dom (Rev f) by FINSEQ_1:def 3;
then A10: ( (Rev f) . i = f . (((len f) - i) + 1) & (Rev f) . (i + 1) = f . (((len f) - (i + 1)) + 1) ) by A6, FINSEQ_5:def 3;
((len f) - (i + 1)) + 1 = (len f) - i ;
then reconsider j = (len f) - i as Element of NAT by A4, A8, FINSEQ_5:1;
((len f) - (i + 1)) + 1 in Seg (len f) by A4, A9, FINSEQ_5:2;
then A11: j >= 1 by FINSEQ_1:3;
((len f) - i) + 1 in Seg (len f) by A4, A5, FINSEQ_5:2;
then j + 1 <= len f by FINSEQ_1:3;
then j < len f by NAT_1:13;
hence (Rev f) . i <> (Rev f) . (i + 1) by A1, A10, A11, Def2; :: thesis: verum