theorem :: FINSEQ_4:13

for f being Function
for x being object st f is_one-to-one_at x holds
f <- (f . x) = x