let X be VectSp of F_Real ; :: thesis: for v, w being Element of X
for v1, w1 being Element of (RVSp2RLSp X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
let v, w be Element of X; :: thesis: for v1, w1 being Element of (RVSp2RLSp X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
let v1, w1 be Element of (RVSp2RLSp X); :: thesis: ( v = v1 & w = w1 implies ( v + w = v1 + w1 & v - w = v1 - w1 ) )
assume AS: ( v = v1 & w = w1 ) ; :: thesis: ( v + w = v1 + w1 & v - w = v1 - w1 )
- w1 = (- 1) * w1 by RLVECT_1:16
.= (- (1. F_Real)) * w by AS
.= - w by VECTSP_1:14 ;
hence ( v + w = v1 + w1 & v - w = v1 - w1 ) by AS; :: thesis: verum