let f be FinSequence; :: thesis: ( f is one-to-one implies f is almost-one-to-one )
assume A1: f is one-to-one ; :: thesis: f is almost-one-to-one
let i, j be Element of NAT ; :: according to JORDAN23:def 1 :: thesis: ( i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f . i = f . j implies i = j )
assume that
A2: i in dom f and
A3: j in dom f and
( i <> 1 or j <> len f ) and
( i <> len f or j <> 1 ) and
A4: f . i = f . j ; :: thesis: i = j
thus i = j by A1, A2, A3, A4, FUNCT_1:def 4; :: thesis: verum