let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions (X,T))
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let T be NormedLinearTopSpace; :: thesis: for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions (X,T))
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let x1, x2 be Point of (R_Normed_Space_of_C_0_Functions (X,T)); :: thesis: for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let y1, y2 be Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)); :: 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 addF of (RealVectSpace ( the carrier of X,T)) || (C_0_Functions (X,T))) . [x1,x2] by RSSPACE:def 8
.= the addF of (RealVectSpace ( the carrier of X,T)) . [x1,x2] by FUNCT_1:49
.= ( the addF of (RealVectSpace ( the carrier of X,T)) || (BoundedFunctions ( the carrier of X,T))) . [y1,y2] by A1, FUNCT_1:49
.= y1 + y2 by RSSPACE:def 8, RSSPACE4:6 ; :: thesis: verum