theorem Th10: :: AMI_8:10

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