let a be Complex; :: thesis: for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = |.a.| * ||.F.||
let X be non empty compact TopSpace; :: thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = |.a.| * ||.F.||
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ||.(a * F).|| = |.a.| * ||.F.||
reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3
.= |.a.| * ||.F1.|| by CC0SP1:25
.= |.a.| * ||.F.|| by FUNCT_1:49 ; :: thesis: verum