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