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

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