let dl be Int-Location ; :: thesis: ex i being Element of NAT st dl = intloc i
dl in SCM+FSA-Data-Loc by Def4;
then reconsider D = dl as Data-Location by AMI_3:def 2;
consider i being Element of NAT such that
A1: D = dl. i by AMI_5:18;
take i ; :: thesis: dl = intloc i
thus dl = intloc i by A1; :: thesis: verum