theorem :: SCMRING3:8

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