let V be RealLinearSpace; :: thesis: for o, v, w being Element of V
for b, a2, a3 being Real holds ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))
let o, v, w be Element of V; :: thesis: for b, a2, a3 being Real holds ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))
let b, a2, a3 be Real; :: thesis: ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))
thus ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = ((0. V) + ((b * a2) * v)) + (((- b) * a3) * w) by RLVECT_1:10
.= ((b * a2) * v) + (((- b) * a3) * w) by RLVECT_1:4
.= (b * (a2 * v)) + ((b * (- a3)) * w) by RLVECT_1:def 7
.= (b * (a2 * v)) + (b * ((- a3) * w)) by RLVECT_1:def 7
.= (b * (a2 * v)) + (b * (- (a3 * w))) by Lm8
.= b * ((a2 * v) - (a3 * w)) by RLVECT_1:def 5 ; :: thesis: verum