( len (Line (M,i)) = width M & Line (M,i) is Element of D * ) by Def7, 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