let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds
f + g = f1 + g1
let Y be RealNormSpace; :: thesis: for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds
f + g = f1 + g1
let f, g be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds
f + g = f1 + g1
let f1, g1 be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: ( f1 = f & g1 = g implies f + g = f1 + g1 )
assume A1: ( f1 = f & g1 = g ) ; :: thesis: f + g = f1 + g1
reconsider f2 = f, g2 = g as Point of (R_VectorSpace_of_ContinuousFunctions (X,Y)) ;
reconsider f3 = f2, g3 = g2 as Point of (R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;
A2: R_VectorSpace_of_ContinuousFunctions (X,Y) is Subspace of R_VectorSpace_of_BoundedFunctions (X,Y) by RSSPACE:11;
thus f + g = f2 + g2
.= f3 + g3 by A2, RLSUB_1:13
.= f1 + g1 by A1 ; :: thesis: verum