theorem Th14: :: JORDAN23:14

for D being non empty set
for f being FinSequence of D holds
( f is almost-one-to-one iff ( f /^ 1 is one-to-one & f | ((len f) -' 1) is one-to-one ) )