let dl be Int-Location; :: thesis: ex i being Nat st dl = intloc i
dl in SCM-Data-Loc by AMI_2:def 16;
then reconsider D = dl as Data-Location ;
consider i being Nat such that
A1: D = dl. i by AMI_5:1;
take i ; :: thesis: dl = intloc i
thus dl = intloc i by A1; :: thesis: verum