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_1:26;
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_1:def 8;
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