( dom p = n & rng p c= X ) by FUNCT_2:def 1;
then reconsider P = p as XFinSequence by AFINSQ_1:5;
reconsider P = P as XFinSequence of X ;
len P = n by FUNCT_2:def 1;
hence p is n -element XFinSequence of X by CARD_1:def 7; :: thesis: verum