let X be non empty TopSpace; :: thesis: for x1, x2 being Point of (C_Normed_Space_of_C_0_Functions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let x1, x2 be Point of (C_Normed_Space_of_C_0_Functions X); :: thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 )
A1: CC_0_Functions X is add-closed by Th38;
A2: ComplexBoundedFunctions the carrier of X is add-closed by CC0SP1:def 2;
assume A3: ( x1 = y1 & x2 = y2 ) ; :: thesis: x1 + x2 = y1 + y2
thus x1 + x2 = ( the addF of (ComplexVectSpace the carrier of X) || (CC_0_Functions X)) . [x1,x2] by A1, C0SP1:def 5
.= the addF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the addF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A3, FUNCT_1:49
.= y1 + y2 by A2, C0SP1:def 5 ; :: thesis: verum