theorem :: C0SP3:37

for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for g being Function of S,T st f = g holds
for t being Point of S holds ||.(g . t).|| <= ||.f.||