let R be good Ring; :: thesis: for dl being Data-Location of R ex i being Element of NAT st dl = dl. (R,i)
let dl be Data-Location of R; :: thesis: ex i being Element of NAT st dl = dl. (R,i)
dl in Data-Locations SCM by SCMRING2:1;
then consider i being Element of NAT such that
A1: dl = [1,i] by AMI_2:32, AMI_3:72;
take i ; :: thesis: dl = dl. (R,i)
thus dl = dl. (R,i) by A1, Th3; :: thesis: verum