let R be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let a be Element of R; for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R; for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let v, u, w be Element of V; 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 VECTSP_1:def 14
.=
((a * v) + (a * u)) + (a * w)
by VECTSP_1:def 14
; verum