theorem :: FINSEQ_4:10

for f being Function
for y being object st f just_once_values y holds
Im (f,(f <- y)) = {y}