let D be set ; :: thesis: for f being FinSequence of D holds
( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j )
let f be FinSequence of D; :: thesis: ( f is almost-one-to-one iff for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j )
thus ( f is almost-one-to-one implies for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j ) :: thesis: ( ( for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j ) implies f is almost-one-to-one )

proof

assume A1: f is almost-one-to-one ; :: thesis: for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j
let i, j be Element of NAT ; :: 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 & j in dom f ) and
A3: ( i <> 1 or j <> len f ) and
A4: ( i <> len f or j <> 1 ) and
A5: f /. i = f /. j ; :: thesis: i = j
f . i = f /. j by A2, A5, PARTFUN1:def 8
.= f . j by A2, PARTFUN1:def 8 ;
hence i = j by A1, A2, A3, A4, Def1; :: thesis: verum

end;

assume A6: for i, j being Element of NAT st i in dom f & j in dom f & ( i <> 1 or j <> len f ) & ( i <> len f or j <> 1 ) & f /. i = f /. j holds
i = j ; :: thesis: f is almost-one-to-one

now

let i, j be Element of NAT ; :: 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
A7: ( i in dom f & j in dom f ) and
A8: ( i <> 1 or j <> len f ) and
A9: ( i <> len f or j <> 1 ) and
A10: f . i = f . j ; :: thesis: i = j
f /. i = f . j by A7, A10, PARTFUN1:def 8
.= f /. j by A7, PARTFUN1:def 8 ;
hence i = j by A6, A7, A8, A9; :: thesis: verum

end;

hence f is almost-one-to-one by Def1; :: thesis: verum