let R be Ring; :: thesis: for a being Data-Location of R holds Values a = the carrier of R
let a be Data-Location of R; :: thesis: Values a = the carrier of R
( a in Data-Locations & the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK ) by SCMRING2:1, SCMRING2:24;
hence Values a = the carrier of R by AMI_3:27, SCMRING1:4; :: thesis: verum