let V be RealLinearSpace; 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; 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; ( v = (b1 * x) + (b2 * y) implies a * v = ((a * b1) * x) + ((a * b2) * y) )
assume
v = (b1 * x) + (b2 * y)
; 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
;
verum