let S be non empty compact TopSpace; :: thesis: 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.||
let T be NormedLinearTopSpace; :: thesis: 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.||
let f be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for g being Function of S,T st f = g holds
for t being Point of S holds ||.(g . t).|| <= ||.f.||
let g be Function of S,T; :: thesis: ( f = g implies for t being Point of S holds ||.(g . t).|| <= ||.f.|| )
assume A1: f = g ; :: thesis: for t being Point of S holds ||.(g . t).|| <= ||.f.||
then g in BoundedFunctions ( the carrier of S,T) by Th34;
then reconsider h = g as bounded Function of the carrier of S,T by RSSPACE4:def 5;
reconsider k = h as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by Th34, A1;
||.k.|| = ||.f.|| by A1, FUNCT_1:49;
hence for t being Point of S holds ||.(g . t).|| <= ||.f.|| by RSSPACE4:16; :: thesis: verum