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