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 holds a * (Sum (<*> the carrier of V)) = 0. V

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 holds a * (Sum (<*> the carrier of V)) = 0. V

let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R; :: thesis: a * (Sum (<*> the carrier of V)) = 0. V

thus a * (Sum (<*> the carrier of V)) = a * (0. V) by RLVECT_1:43

.= 0. V by VECTSP_1:14 ; :: thesis: verum

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R holds a * (Sum (<*> the carrier of V)) = 0. V

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 holds a * (Sum (<*> the carrier of V)) = 0. V

let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R; :: thesis: a * (Sum (<*> the carrier of V)) = 0. V

thus a * (Sum (<*> the carrier of V)) = a * (0. V) by RLVECT_1:43

.= 0. V by VECTSP_1:14 ; :: thesis: verum