reconsider X = {0,1,2} as non empty set ;
consider a1 being Element of X, k being Element of NAT such that
A1: a = [a1,k] by DOMAIN_1:1;
( a1 = 0 or a1 = 1 or a1 = 2 ) by ENUMSET1:def 1;
hence a `1 is Nat by A1; :: thesis: verum