( len (Line M,i) = width M & Line M,i is Element of D * ) by Def8, FINSEQ_1:def 11;
then Line M,i in { p where p is Element of D * : len p = width M } ;
hence Line M,i is Element of (width M) -tuples_on D ; :: thesis: verum