let V be ComplexLinearSpace; :: thesis: 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; :: thesis: for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
let z be Complex; :: thesis: 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 ; :: thesis: verum