theorem Lem12: :: MSAFREE5:7

for a being object
for F being Function-yielding Function
for f being Function holds doms (F +* (a,f)) = (doms F) +* (a,(dom f))