theorem Th7: :: PYTHTRIP:7

for k, m, n being Element of NAT holds
( ( m divides n or k = 0 ) iff k * m divides k * n )