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:23;
take i ; :: thesis: dl = DataLoc (i,0)
thus dl = DataLoc (i,0) by A1, ABSVALUE:def 1; :: thesis: verum