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