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

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