let n, m be Nat; :: thesis: for D being non empty set
for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg n holds
( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
let D be non empty set ; :: thesis: for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg n holds
( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
let l be Nat; :: thesis: for M being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg n holds
( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
let M be Matrix of n,m,D; :: thesis: for pD being FinSequence of D
for i being Nat st i in Seg n holds
( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
let pD be FinSequence of D; :: thesis: for i being Nat st i in Seg n holds
( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
let i be Nat; :: thesis: ( i in Seg n implies ( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) ) )
assume A1: i in Seg n ; :: thesis: ( ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) & ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) ) )
set R = RLine (M,l,pD);
set LR = Line ((RLine (M,l,pD)),i);
thus ( i = l & len pD = width M implies Line ((RLine (M,l,pD)),i) = pD ) :: thesis: ( i <> l implies Line ((RLine (M,l,pD)),i) = Line (M,i) )

proof

assume that
A2: i = l and
A3: len pD = width M ; :: thesis: Line ((RLine (M,l,pD)),i) = pD
A4: width (RLine (M,l,pD)) = len pD by A3, Def3;

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

let j be Nat; :: thesis: ( 1 <= j & j <= len pD implies (Line ((RLine (M,l,pD)),i)) . j = pD . j )
assume that
A6: 1 <= j and
A7: j <= len pD ; :: thesis: (Line ((RLine (M,l,pD)),i)) . j = pD . j
A8: j in Seg (width (RLine (M,l,pD))) by A4, A6, A7;
n = len (RLine (M,l,pD)) by MATRIX_0:def 2;
then i in dom (RLine (M,l,pD)) by A1, FINSEQ_1:def 3;
then A9: [i,j] in Indices (RLine (M,l,pD)) by A8, ZFMISC_1:87;
A10: Indices (RLine (M,l,pD)) = Indices M by Lm4;
(Line ((RLine (M,l,pD)),i)) . j = (RLine (M,l,pD)) * (i,j) by A8, MATRIX_0:def 7;
hence (Line ((RLine (M,l,pD)),i)) . j = pD . j by A2, A3, A9, A10, Def3; :: thesis: verum

end;

len (Line ((RLine (M,l,pD)),i)) = len pD by A4, MATRIX_0:def 7;
hence Line ((RLine (M,l,pD)),i) = pD by A5; :: thesis: verum

end;

set LM = Line (M,i);
A11: width M = len (Line (M,i)) by MATRIX_0:def 7;
A12: width M = width (RLine (M,l,pD)) by Lm4;
assume A13: i <> l ; :: thesis: Line ((RLine (M,l,pD)),i) = Line (M,i)

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

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line (M,i)) implies (Line (M,i)) . j = (Line ((RLine (M,l,pD)),i)) . j )
assume that
A15: 1 <= j and
A16: j <= len (Line (M,i)) ; :: thesis: (Line (M,i)) . j = (Line ((RLine (M,l,pD)),i)) . j
A17: j in Seg (len (Line (M,i))) by A15, A16;
then A18: (Line (M,i)) . j = M * (i,j) by A11, MATRIX_0:def 7;
i in Seg (len M) by A1, MATRIX_0:def 2;
then i in dom M by FINSEQ_1:def 3;
then A19: [i,j] in Indices M by A11, A17, ZFMISC_1:87;
A20: (Line ((RLine (M,l,pD)),i)) . j = (RLine (M,l,pD)) * (i,j) by A12, A11, A17, MATRIX_0:def 7;

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

per cases ( len pD = width M or len pD <> width M ) ;

case len pD = width M ; :: thesis: (Line (M,i)) . j = (Line ((RLine (M,l,pD)),i)) . j

hence (Line (M,i)) . j = (Line ((RLine (M,l,pD)),i)) . j by A13, A18, A20, A19, Def3; :: thesis: verum

end;

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

hence (Line (M,i)) . j = (Line ((RLine (M,l,pD)),i)) . j by Def3; :: thesis: verum

end;

end;

end;

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

end;

len (Line ((RLine (M,l,pD)),i)) = width (RLine (M,l,pD)) by MATRIX_0:def 7;
hence Line ((RLine (M,l,pD)),i) = Line (M,i) by A12, A11, A14; :: thesis: verum