let R be non trivial Ring; :: thesis: for dl being Data-Location of R ex i being Nat st dl = dl. (R,i)
let dl be Data-Location of R; :: thesis: ex i being Nat st dl = dl. (R,i)
dl in Data-Locations by SCMRING2:1;
then consider i being 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, Th1; :: thesis: verum