set qK = Line M,k;
set pK = Line M,l;
set M1 = RLine M,l,((a * (Line M,k)) + (Line M,l));
take RLine M,l,((a * (Line M,k)) + (Line M,l)) ; :: thesis: ( len (RLine M,l,((a * (Line M,k)) + (Line M,l))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies (RLine M,l,((a * (Line M,k)) + (Line M,l))) * i,j = (a * (M * k,j)) + (M * l,j) ) & ( i <> l implies (RLine M,l,((a * (Line M,k)) + (Line M,l))) * i,j = M * i,j ) ) ) )
len M = n by MATRIX_1:26;
then ( len ((a * (Line M,k)) + (Line M,l)) = width M & dom M = Seg n ) by FINSEQ_1:def 3, FINSEQ_1:def 18;
hence ( len (RLine M,l,((a * (Line M,k)) + (Line M,l))) = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies (RLine M,l,((a * (Line M,k)) + (Line M,l))) * i,j = (a * (M * k,j)) + (M * l,j) ) & ( i <> l implies (RLine M,l,((a * (Line M,k)) + (Line M,l))) * i,j = M * i,j ) ) ) ) by A1, Lm3, MATRIX11:def 3; :: thesis: verum