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