theorem Th30: :: ORDINAL4:30

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