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_0:25;
then ( len ((a * (Line (M,k))) + (Line (M,l))) = width M & dom M = Seg n ) by CARD_1:def 7, FINSEQ_1:def 3;
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