:: deftheorem defines =0_goto SCMRING2:def 9 :
for R being Ring
for l being Nat
for a being Data-Location of R holds a =0_goto l = [7,<*l*>,<*a*>];