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