let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for F being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) holds 0 <= ||.F.||
let T be NormedLinearTopSpace; :: thesis: for F being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) holds 0 <= ||.F.||
let F be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: 0 <= ||.F.||
reconsider F1 = F as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by Th34;
||.F.|| = ||.F1.|| by FUNCT_1:49;
hence 0 <= ||.F.|| ; :: thesis: verum