theorem :: ORDINAL3:63

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