:: deftheorem defines := SCMRING2:def 7 :
for R being Ring
for a being Data-Location of R
for r being Element of R holds a := r = [5,{},<*a,r*>];