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

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