theorem Th28: :: ARYTM_3:28

for a, b, c being natural Ordinal st c <> {} holds
RED ((a *^ c),(b *^ c)) = RED (a,b)