1 <= n by NAT_1:14;
then A2: n in Seg m by A1;
len X = m by CARD_1:def 7;
then n in dom X by A2, FINSEQ_1:def 3;
hence X . n is non empty set ; :: thesis: verum