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