( len (0* (K,n)) = n & 0* (K,n) in the carrier of K * ) by CARD_1:def 7, FINSEQ_1:def 11;
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