let x be set ; :: thesis: ( x in SCM-Data-Loc implies ex k being Element of NAT st x = [1,k] )
assume x in SCM-Data-Loc ; :: thesis: ex k being Element of NAT st x = [1,k]
then consider y, z being set such that
A1: y in {1} and
A2: z in NAT and
A3: x = [y,z] by ZFMISC_1:84;
reconsider k = z as Element of NAT by A2;
take k ; :: thesis: x = [1,k]
thus x = [1,k] by A1, A3, TARSKI:def 1; :: thesis: verum