dom (Det R) = dom R by Def7;
then len (Det R) = len R by FINSEQ_3:29;
hence Det R is Element of (len R) -tuples_on the carrier of K by FINSEQ_2:92; :: thesis: verum