let V be RealLinearSpace; :: thesis: for p, q, v being Element of V

for a, b being Real st p + (a * v) = q + (b * v) holds

((a - b) * v) + p = q

let p, q, v be Element of V; :: thesis: for a, b being Real st p + (a * v) = q + (b * v) holds

((a - b) * v) + p = q

let a, b be Real; :: thesis: ( p + (a * v) = q + (b * v) implies ((a - b) * v) + p = q )

assume p + (a * v) = q + (b * v) ; :: thesis: ((a - b) * v) + p = q

then (p + (a * v)) + (- (b * v)) = q + ((b * v) + (- (b * v))) by RLVECT_1:def 3

.= q + (0. V) by RLVECT_1:5

.= q ;

then q = p + ((a * v) + (- (b * v))) by RLVECT_1:def 3

.= p + ((a * v) - (b * v)) by RLVECT_1:def 11

.= p + ((a - b) * v) by RLVECT_1:35 ;

hence ((a - b) * v) + p = q ; :: thesis: verum

for a, b being Real st p + (a * v) = q + (b * v) holds

((a - b) * v) + p = q

let p, q, v be Element of V; :: thesis: for a, b being Real st p + (a * v) = q + (b * v) holds

((a - b) * v) + p = q

let a, b be Real; :: thesis: ( p + (a * v) = q + (b * v) implies ((a - b) * v) + p = q )

assume p + (a * v) = q + (b * v) ; :: thesis: ((a - b) * v) + p = q

then (p + (a * v)) + (- (b * v)) = q + ((b * v) + (- (b * v))) by RLVECT_1:def 3

.= q + (0. V) by RLVECT_1:5

.= q ;

then q = p + ((a * v) + (- (b * v))) by RLVECT_1:def 3

.= p + ((a * v) - (b * v)) by RLVECT_1:def 11

.= p + ((a - b) * v) by RLVECT_1:35 ;

hence ((a - b) * v) + p = q ; :: thesis: verum