let dl be Int_position; :: thesis: ex i being Nat st dl = DataLoc (i,0)
consider i being Nat such that
A1: dl = [1,i] by AMI_2:23, AMI_2:def 16;
take i ; :: thesis: dl = DataLoc (i,0)
thus dl = DataLoc (i,0) by A1, ABSVALUE:def 1; :: thesis: verum