let X be non empty compact TopSpace; :: thesis: for a being Complex
for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let a be Complex; :: thesis: for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let x be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let y be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; :: thesis: a * x = a * y
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
thus a * x = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [a1,x] by CC0SP1:def 3
.= the Mult of (CAlgebra the carrier of X) . [a1,x] by FUNCT_1:49
.= ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(ComplexBoundedFunctions the carrier of X):]) . [a1,y] by A1, FUNCT_1:49
.= a * y by CC0SP1:def 3 ; :: thesis: verum