theorem Th46: :: ORDINAL3:46

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