theorem :: C0SP3:48

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G, H being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for f, g, h being Function of S,T st f = F & g = G & h = H holds
( H = F - G iff for x being Element of S holds h . x = (f . x) - (g . x) )