consider i, j being Nat such that
A1: i in dom f and
A2: j in dom f and
A3: f . i <> f . j by SEQM_3:def 10;
A4: i <= len f by A1, FINSEQ_3:25;
j <= len f by A2, FINSEQ_3:25;
then reconsider k1 = (len f) - i, l1 = (len f) - j as Element of NAT by A4, INT_1:5;
take k = k1 + 1; :: according to SEQM_3:def 10 :: thesis: ex b₁ being set 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:59; :: 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:59; :: 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