for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))