theorem Th72: :: VALUED_2:72

for x being object
for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)