let n, m, l 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) & len M = len (RLine M,l,(Line M,l)) ) by Lm4, MATRIX_1:def 8;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len M implies (RLine M,l,(Line M,l)) . i = M . i )
assume A2: ( 1 <= i & i <= len M ) ; :: thesis: (RLine M,l,(Line M,l)) . i = M . i
i in NAT by ORDINAL1:def 13;
then A3: ( i in Seg (len M) & n = len M ) by A2, MATRIX_1:def 3;
then A4: ( Line M,i = M . i & (RLine M,l,(Line M,l)) . i = Line (RLine M,l,(Line M,l)),i ) by MATRIX_2:10;

now

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, A3, A4, 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 A3, A4, Th28; :: thesis: verum

end;

end;

end;

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

end;

hence M = RLine M,l,(Line M,l) by A1, FINSEQ_1:18; :: thesis: verum