let n1, n2 be Element of NAT ; :: thesis: DataLoc n1,n2 = intpos (n1 + n2)
A1: n1 + n2 >= 0 by NAT_1:2;
thus DataLoc n1,n2 = [1,(abs (n1 + n2))] by SCMPDS_2:def 4
.= [1,(n1 + n2)] by A1, ABSVALUE:def 1
.= intpos (n1 + n2) ; :: thesis: verum