let a be Int_position; :: thesis: ex i being Nat st a = intpos i
a in SCM-Data-Loc by AMI_2:def 16;
then consider x, y being object such that
A1: x in {1} and
A2: y in NAT and
A3: a = [x,y] by ZFMISC_1:84;
reconsider k = y as Nat by A2;
take k ; :: thesis: a = intpos k
thus intpos k = dl. k by SCMP_GCD:def 1
.= a by A1, A3, TARSKI:def 1 ; :: thesis: verum