theorem :: FINSEQ_4:14

for f being Function
for y being object st f just_once_values y holds
f is_one-to-one_at f <- y