theorem Th5: :: BASEL_2:5

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a, b, c, d being Element of L holds <%a,b%> *' <%c,d%> = <%(a * c),((a * d) + (b * c)),(b * d)%>