let X be non empty compact TopSpace; :: thesis: for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
let x1, x2 be Point of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
let y1, y2 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( x1 = y1 & x2 = y2 implies x1 * x2 = y1 * y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; :: thesis: x1 * x2 = y1 * y2
thus x1 * x2 = ( the multF of (RAlgebra the carrier of X) || (ContinuousFunctions X)) . [x1,x2] by C0SP1:def 6
.= the multF of (RAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the multF of (RAlgebra the carrier of X) || (BoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 * y2 by C0SP1:def 6 ; :: thesis: verum