let a be Real; 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; 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; 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)); ( ( ||.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; ( ||.(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
; ||.(F + G).|| <= ||.F.|| + ||.G.||
thus
||.(F + G).|| <= ||.F.|| + ||.G.||
by A1, A2, A3, NORMSP_1:def 1; verum