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

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