let D be set ; :: thesis: for f being FinSequence of D holds
( f is almost-one-to-one iff for i, j being 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 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 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 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 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 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 and
A3: j in dom f and
A4: ( i <> 1 or j <> len f ) and
A5: ( i <> len f or j <> 1 ) and
A6: f /. i = f /. j ; :: thesis: i = j
f . i = f /. j by A2, A6, PARTFUN1:def 6
.= f . j by A3, PARTFUN1:def 6 ;
hence i = j by A1, A2, A3, A4, A5; :: thesis: verum

end;

assume A7: for i, j being 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 :: thesis: for i, j being 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 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
A8: i in dom f and
A9: j in dom f and
A10: ( i <> 1 or j <> len f ) and
A11: ( i <> len f or j <> 1 ) and
A12: f . i = f . j ; :: thesis: i = j
f /. i = f . j by A8, A12, PARTFUN1:def 6
.= f /. j by A9, PARTFUN1:def 6 ;
hence i = j by A7, A8, A9, A10, A11; :: thesis: verum

end;

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