let X be LeftMod of INT.Ring ; :: thesis: for v, w being Element of X
for v1, w1 being Element of (modetrans 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 (modetrans X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
let v1, w1 be Element of (modetrans X); :: thesis: ( v = v1 & w = w1 implies ( v + w = v1 + w1 & v - w = v1 - w1 ) )
assume A1: ( v = v1 & w = w1 ) ; :: thesis: ( v + w = v1 + w1 & v - w = v1 - w1 )
thus v + w = v1 + w1 by A1; :: thesis: v - w = v1 - w1
A2: - w1 = (- 1) * w1 by ZMODUL01:2
.= (- (1. INT.Ring)) * w by A1
.= - w by VECTSP_1:14 ;
thus v - w = v1 - w1 by A1, A2; :: thesis: verum