theorem Th2: :: VECTSP_1:6

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x being Element of F holds x * (0. F) = 0. F