let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed VectSp-like VectSpStr of 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 VectSp-like VectSpStr of R holds a * (Sum (<*> the carrier of V)) = 0. V
let V be non empty right_complementable Abelian add-associative right_zeroed VectSp-like VectSpStr of R; :: thesis: a * (Sum (<*> the carrier of V)) = 0. V
thus a * (Sum (<*> the carrier of V)) = a * (0. V) by RLVECT_1:60
.= 0. V by VECTSP_1:59 ; :: thesis: verum