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_{1} being set st

( k in dom (Rev f) & b_{1} in dom (Rev f) & not (Rev f) . k = (Rev f) . b_{1} )

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

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

( k in dom (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