set g = Rev f;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (Rev f) or not x2 in dom (Rev f) or not (Rev f) . x1 = (Rev f) . x2 or x1 = x2 )
assume that
A1: x1 in dom (Rev f) and
A2: x2 in dom (Rev f) and
A3: (Rev f) . x1 = (Rev f) . x2 ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A1, A2;
A4: len (Rev f) = len f by Def3;
then ( i1 <= len f & i2 <= len f ) by A1, A2, FINSEQ_3:25;
then reconsider i19 = ((len f) - i1) + 1, i29 = ((len f) - i2) + 1 as Element of NAT by Th1;
A5: f . i19 = (Rev f) . x1 by A1, Def3
.= f . i29 by A2, A3, Def3 ;
( dom (Rev f) = Seg (len (Rev f)) & dom f = Seg (len f) ) by FINSEQ_1:def 3;
then ( i19 in dom f & i29 in dom f ) by A1, A2, A4, Th2;
then i19 = i29 by A5, FUNCT_1:def 4;
hence x1 = x2 ; :: thesis: verum