theorem Th26: :: CC0SP1:26

for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )