theorem :: FINSEQ_4:12

for f being Function
for y being object st f is one-to-one & y in rng f holds
(f ") . y = f <- y