theorem :: SCMRING3:5
for R being Ring
for a, b being Data-Location of R holds InsCode (a := b) = 1 ;