set pK = Line (M,l);
set M1 = RLine (M,l,(a * (Line (M,l))));
take RLine (M,l,(a * (Line (M,l)))) ; :: thesis: ( len (RLine (M,l,(a * (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,l))))) * (i,j) = a * (M * (l,j)) ) & ( i <> l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) )
len M = n by MATRIX_0:25;
then A1: dom M = Seg n by FINSEQ_1:def 3;
( len (Line (M,l)) = width M & len (a * (Line (M,l))) = len (Line (M,l)) ) by MATRIXR1:16, MATRIX_0:def 7;
hence ( len (RLine (M,l,(a * (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,l))))) * (i,j) = a * (M * (l,j)) ) & ( i <> l implies (RLine (M,l,(a * (Line (M,l))))) * (i,j) = M * (i,j) ) ) ) ) by A1, Lm2, MATRIX11:def 3; :: thesis: verum