let X be non empty compact TopSpace; :: thesis: for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( x1 = y1 & x2 = y2 implies x1 - x2 = y1 - y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; :: thesis: x1 - x2 = y1 - y2
reconsider z2 = x2 as VECTOR of (C_Normed_Algebra_of_ContinuousFunctions X) ;
reconsider e = - 1r as Complex ;
- x2 = e * x2 by CLVECT_1:3
.= e * y2 by A1, Lm5
.= - y2 by CLVECT_1:3 ;
hence x1 - x2 = y1 - y2 by A1, Lm4; :: thesis: verum