theorem Th12: :: AMI_8:12

for j, m, n being Nat st m <> j holds
MultBy ((dl. m),(dl. n)) is j -dl.constant