theorem :: ORDINAL3:50

for A, B, C being Ordinal holds (A *^ B) *^ C = A *^ (B *^ C)