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))))
; ( 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; verum