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