let a be Real; :: thesis: for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F, G being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) & ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for F, G being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) & ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let T be NormedLinearTopSpace; :: thesis: for F, G being Point of (R_NormSpace_of_ContinuousFunctions (S,T)) holds
( ( ||.F.|| = 0 implies F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) & ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) & ( F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
reconsider F1 = F, G1 = G as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by Th34;
A1: ||.F.|| = ||.F1.|| by FUNCT_1:49;
A2: ||.G.|| = ||.G1.|| by FUNCT_1:49;
A3: ||.(F + G).|| = ||.(F1 + G1).|| by Th38, Th36;
( ||.F1.|| = 0 iff F1 = 0. (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) ) by NORMSP_0:def 5;
hence ( ||.F.|| = 0 iff F = 0. (R_NormSpace_of_ContinuousFunctions (S,T)) ) by FUNCT_1:49, Th41; :: thesis: ( ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
thus ||.(a * F).|| = ||.(a * F1).|| by Th39, Th36
.= |.a.| * ||.F1.|| by NORMSP_1:def 1
.= |.a.| * ||.F.|| by FUNCT_1:49 ; :: thesis: ||.(F + G).|| <= ||.F.|| + ||.G.||
thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, NORMSP_1:def 1; :: thesis: verum