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 SCM-Data-Loc by SCMRING2:1;
then consider i being Element of NAT such that
A1: dl = [1,i] by AMI_2:32;
take i ; :: thesis: dl = dl. R,i
thus dl = dl. R,i by A1, Th16; :: thesis: verum