for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b holds
a divides b * c