let X be non empty closed_interval Subset of REAL; 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; 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)); 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)); ( f1 = f & g1 = g implies f + g = f1 + g1 )
assume A1:
( f1 = f & g1 = g )
; 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
; verum