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