let V be RealLinearSpace; :: thesis: for v, x, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
let v, x, y be VECTOR of V; :: thesis: for b1, b2, a being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
let b1, b2, a be Real; :: thesis: ( v = (b1 * x) + (b2 * y) implies a * v = ((a * b1) * x) + ((a * b2) * y) )
assume v = (b1 * x) + (b2 * y) ; :: thesis: a * v = ((a * b1) * x) + ((a * b2) * y)
hence a * v = (a * (b1 * x)) + (a * (b2 * y)) by RLVECT_1:def 8
.= ((a * b1) * x) + (a * (b2 * y)) by RLVECT_1:def 10
.= ((a * b1) * x) + ((a * b2) * y) by RLVECT_1:def 10 ;
:: thesis: verum