theorem Th17: :: ARYTM_3:17

for a, b, c being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c