let V be RealLinearSpace; :: thesis: for v, w being Element of V
for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
let v, w be Element of V; :: thesis: for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
let a, b be Real; :: thesis: ( (a * v) + (b * w) = 0. V implies a * v = (- b) * w )
assume (a * v) + (b * w) = 0. V ; :: thesis: a * v = (- b) * w
then a * v = - (b * w) by RLVECT_1:6
.= b * (- w) by RLVECT_1:25 ;
hence a * v = (- b) * w by RLVECT_1:24; :: thesis: verum