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

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