let V be RealLinearSpace; :: thesis: for a being Real
for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let a be Real; :: thesis: for v, u being VECTOR of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)
let v, u be VECTOR of V; :: thesis: a * (Sum <*v,u*>) = (a * v) + (a * u)
thus a * (Sum <*v,u*>) = a * (v + u) by Th45
.= (a * v) + (a * u) by Def5 ; :: thesis: verum