theorem :: FUNCT_1:20

for X being set
for x being object
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x