theorem Th23: :: CARD_2:24
for K, M, N being Cardinal holds K *` (M +` N) = (K *` M) +` (K *` N)