let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for x1, x2 being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let T be NormedLinearTopSpace; :: thesis: for x1, x2 being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let x1, x2 be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for y1, y2 being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let y1, y2 be Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)); :: thesis: ( x1 = y1 & x2 = y2 implies x1 - x2 = y1 - y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; :: thesis: x1 - x2 = y1 - y2
- x2 = (- 1) * x2 by RLVECT_1:16
.= (- 1) * y2 by A1, Th39
.= - y2 by RLVECT_1:16 ;
hence x1 - x2 = y1 - y2 by A1, Th38; :: thesis: verum