let dl be Int_position ; :: thesis: ex i being Element of NAT st dl = DataLoc i,0
dl in SCM-Data-Loc by SCMPDS_2:def 2;
then consider i being Element of NAT such that
A1: dl = [1,i] by AMI_2:32;
take i ; :: thesis: dl = DataLoc i,0
thus dl = DataLoc i,0 by A1, ABSVALUE:def 1; :: thesis: verum