let V be ComplexLinearSpace; for u, v1, v2 being VECTOR of V
for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
let u, v1, v2 be VECTOR of V; for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
let z be Complex; z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
thus z * (Sum <*u,v1,v2*>) =
z * ((u + v1) + v2)
by RLVECT_1:46
.=
(z * (u + v1)) + (z * v2)
by Def2
.=
((z * u) + (z * v1)) + (z * v2)
by Def2
; verum