let n1, n2 be Nat; :: thesis: DataLoc (n1,n2) = intpos (n1 + n2)
thus DataLoc (n1,n2) = [1,|.(n1 + n2).|] by SCMPDS_2:def 3
.= [1,(n1 + n2)] by ABSVALUE:def 1
.= intpos (n1 + n2) ; :: thesis: verum