theorem :: SCMRING3:6

for R being Ring
for a, b being Data-Location of R holds InsCode (AddTo (a,b)) = 2 ;