theorem Th6: :: ANPROJ_8:7

for K being non empty right_complementable left_unital associative commutative Abelian add-associative right_zeroed doubleLoopStr
for a1, a2, a3, b1, b2, b3 being Element of K holds <*a1,a2,a3*> "*" <*b1,b2,b3*> = ((a1 * b1) + (a2 * b2)) + (a3 * b3)