let V be RealLinearSpace; :: thesis: for v, x, y being VECTOR of V
for a, b1, b2 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 a, b1, b2 being Real st v = (b1 * x) + (b2 * y) holds
a * v = ((a * b1) * x) + ((a * b2) * y)
let a, b1, b2 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 5
.= ((a * b1) * x) + (a * (b2 * y)) by RLVECT_1:def 7
.= ((a * b1) * x) + ((a * b2) * y) by RLVECT_1:def 7 ;
:: thesis: verum