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