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) by MATRIX_1:def 8;

A2: now

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
i in NAT by ORDINAL1:def 13;
then A5: i in Seg (len M) by A3, A4;
A6: n = len M by MATRIX_1:def 3;
then A7: (RLine M,l,(Line M,l)) . i = Line (RLine M,l,(Line M,l)),i by A5, MATRIX_2:10;
A8: Line M,i = M . i by A5, A6, 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, 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, FINSEQ_1:18; :: thesis: verum