let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for F being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) st F = 0. (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)) st F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) holds
0 = ||.F.||
let F be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies 0 = ||.F.|| )
assume A1: F = 0. (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;
A2: ||.F.|| = ||.F1.|| by FUNCT_1:49;
F = the carrier of S --> (0. T) by A1, Th40;
then F1 = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by RSSPACE4:15;
hence 0 = ||.F.|| by A2; :: thesis: verum