let V be Z_Module; :: thesis: for a being Integer
for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let a be Integer; :: thesis: for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let v, u, w be VECTOR of V; :: thesis: a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
thus a * (Sum <*v,u,w*>) = a * ((v + u) + w) by RLVECT_1:46
.= (a * (v + u)) + (a * w) by Def2
.= ((a * v) + (a * u)) + (a * w) by Def2 ; :: thesis: verum