let R be non trivial 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 by SCMRING2:1;
then consider i being Element of NAT such that
A1: dl = [1,i] by AMI_2:23, AMI_3:27;
take i ; :: thesis: dl = dl. (R,i)
thus dl = dl. (R,i) by A1, Th2; :: thesis: verum