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