for o1, o2 being non empty Ordinal
for L being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr holds Polynom-Ring (o1,(Polynom-Ring (o2,L))), Polynom-Ring ((o1 +^ o2),L) are_isomorphic