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
A2: - g1 = (- 1) * g1 by RLVECT_1:16
.= (- 1) * g by A1, Th19
.= - g by RLVECT_1:16 ;
thus f - g = f1 - g1 by A1, A2, Th18; :: thesis: verum