theorem Th11: :: FINSEQ_4:11

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