let l, n, m be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))
let D be non empty set ; :: thesis: for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))
let M be Matrix of n,m,D; :: thesis: M = RLine (M,l,(Line (M,l)))
set L = Line (M,l);
set RL = RLine (M,l,(Line (M,l)));
A1: width M = len (Line (M,l)) by MATRIX_0:def 7;

A2: now :: thesis: for i being Nat st 1 <= i & i <= len M holds
(RLine (M,l,(Line (M,l)))) . i = M . i

let i be Nat; :: thesis: ( 1 <= i & i <= len M implies (RLine (M,l,(Line (M,l)))) . i = M . i )
assume that
A3: 1 <= i and
A4: i <= len M ; :: thesis: (RLine (M,l,(Line (M,l)))) . i = M . i
A5: i in Seg (len M) by A3, A4;
A6: n = len M by MATRIX_0:def 2;
then A7: (RLine (M,l,(Line (M,l)))) . i = Line ((RLine (M,l,(Line (M,l)))),i) by A5, MATRIX_0:52;
A8: Line (M,i) = M . i by A5, A6, MATRIX_0:52;

now :: thesis: ( ( i = l & (RLine (M,l,(Line (M,l)))) . i = M . i ) or ( i <> l & (RLine (M,l,(Line (M,l)))) . i = M . i ) )

per cases ( i = l or i <> l ) ;

case i = l ; :: thesis: (RLine (M,l,(Line (M,l)))) . i = M . i

hence (RLine (M,l,(Line (M,l)))) . i = M . i by A1, A5, A6, A8, A7, Th28; :: thesis: verum

end;

case i <> l ; :: thesis: (RLine (M,l,(Line (M,l)))) . i = M . i

hence (RLine (M,l,(Line (M,l)))) . i = M . i by A5, A6, A8, A7, Th28; :: thesis: verum

end;

end;

end;

hence (RLine (M,l,(Line (M,l)))) . i = M . i ; :: thesis: verum

end;

len M = len (RLine (M,l,(Line (M,l)))) by Lm4;
hence M = RLine (M,l,(Line (M,l))) by A2; :: thesis: verum