let f be FinSequence; ( f is weakly-one-to-one implies Rev f is weakly-one-to-one )
assume A1:
f is weakly-one-to-one
; Rev f is weakly-one-to-one
A2:
len f = len (Rev f)
by FINSEQ_5:def 3;
let i be Nat; JORDAN23:def 2 ( 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)
; (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; verum