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 Element of 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: dom f = dom (Rev f) by FINSEQ_5:60;
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 A8: ((len f) - i) + 1 in dom f by FINSEQ_1:def 3;
j in Seg (len f) by A3, A7, FINSEQ_1:def 3;
then ((len f) - j) + 1 in Seg (len f) by FINSEQ_5:2;
then A9: ((len f) - j) + 1 in dom f by FINSEQ_1:def 3;
A10: ( not ((len f) - i) + 1 = 1 or not ((len f) - j) + 1 = len f ) by A5, FINSEQ_5:def 3;
A11: ( not ((len f) - i) + 1 = len f or not ((len f) - j) + 1 = 1 ) by A4, FINSEQ_5:def 3;
( (Rev f) . i = f . (((len f) - i) + 1) & (Rev f) . j = f . (((len f) - j) + 1) ) by A2, A3, FINSEQ_5:def 3;
then ((len f) - i) + 1 = ((len f) - j) + 1 by A1, A6, A8, A9, A10, A11, Def1;
hence i = j ; :: thesis: verum