theorem Th4: :: C0SP1:4

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr
for a being Real holds a * (0. V) = 0. V