( len (0* K,n) = n & 0* K,n in the carrier of K * ) by FINSEQ_1:def 11, FINSEQ_1:def 18;
then 0* K,n in { s where s is Element of the carrier of K * : len s = n } ;
hence 0* K,n is Element of n -tuples_on the carrier of K by FINSEQ_2:def 4; :: thesis: verum