theorem Th1: :: VECTSP10:1

for K being non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr
for a being Element of K
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K
for v being Vector of V holds
( (0. K) * v = 0. V & a * (0. V) = 0. V )