consider i, j being Element of NAT such that
A1: i in dom f and
A2: j in dom f and
A3: f . i <> f . j by SEQM_3:def 15;
A4: i <= len f by A1, FINSEQ_3:27;
j <= len f by A2, FINSEQ_3:27;
then reconsider k1 = (len f) - i, l1 = (len f) - j as Element of NAT by A4, INT_1:18;
take k = k1 + 1; :: according to SEQM_3:def 15 :: thesis: ex b₁ being Element of NAT st
( k in dom (Rev f) & b₁ in dom (Rev f) & not (Rev f) . k = (Rev f) . b₁ )
take l = l1 + 1; :: thesis: ( k in dom (Rev f) & l in dom (Rev f) & not (Rev f) . k = (Rev f) . l )
k + i = (len f) + 1 ;
hence k in dom (Rev f) by A1, FINSEQ_5:62; :: thesis: ( l in dom (Rev f) & not (Rev f) . k = (Rev f) . l )
then A5: (Rev f) . k = f . (((len f) - k) + 1) by FINSEQ_5:def 3
.= f . (0 + i) ;
l + j = (len f) + 1 ;
hence l in dom (Rev f) by A2, FINSEQ_5:62; :: thesis: not (Rev f) . k = (Rev f) . l
then (Rev f) . l = f . (((len f) - l) + 1) by FINSEQ_5:def 3
.= f . (0 + j) ;
hence not (Rev f) . k = (Rev f) . l by A3, A5; :: thesis: verum