let dl be Data-Location ; :: thesis: ex i being Element of NAT st dl = dl. i
dl in Data-Locations by AMI_3:27, AMI_3:def 2;
then consider x, y being set such that
A1: x in {1} and
A2: y in NAT and
A3: dl = [x,y] by AMI_3:27, ZFMISC_1:84;
reconsider k = y as Element of NAT by A2;
take k ; :: thesis: dl = dl. k
thus dl = dl. k by A1, A3, TARSKI:def 1; :: thesis: verum