let X be RealLinearSpace; :: thesis: for v, w being Element of X
for v1, w1 being Element of (RLSp2RVSp 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 (RLSp2RVSp X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
let v1, w1 be Element of (RLSp2RVSp 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 )
hence v + w = v1 + w1 ; :: thesis: v - w = v1 - w1
- w = (- 1) * w by RLVECT_1:16
.= (- (1. F_Real)) * w1 by AS
.= - w1 by VECTSP_1:14 ;
hence v - w = v1 - w1 by AS; :: thesis: verum