theorem Th62: :: VALUED_2:62

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)