for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for x1, x2 being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2