dom (Len F) = dom F by Def3;
then len (Len F) = len F by FINSEQ_3:29;
hence Len F is Element of (len F) -tuples_on NAT by FINSEQ_2:92; :: thesis: verum