theorem Th13: :: FUNCT_4:13

for f, g being Function
for x being object st x in dom g holds
(f +* g) . x = g . x