let m, n 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

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
j in NAT by ORDINAL1:def 13;
then A8: j in Seg (width (RLine M,l,pD)) by A4, A6, A7;
n = len (RLine M,l,pD) by MATRIX_1:def 3;
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:106;
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_1:def 8;
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_1:def 8;
hence Line (RLine M,l,pD),i = pD by A5, FINSEQ_1:18; :: thesis: verum

end;

set LM = Line M,i;
A11: width M = len (Line M,i) by MATRIX_1:def 8;
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

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
j in NAT by ORDINAL1:def 13;
then A17: j in Seg (len (Line M,i)) by A15, A16;
then A18: (Line M,i) . j = M * i,j by A11, MATRIX_1:def 8;
i in Seg (len M) by A1, MATRIX_1:def 3;
then i in dom M by FINSEQ_1:def 3;
then A19: [i,j] in Indices M by A11, A17, ZFMISC_1:106;
A20: (Line (RLine M,l,pD),i) . j = (RLine M,l,pD) * i,j by A12, A11, A17, MATRIX_1:def 8;

now

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_1:def 8;
hence Line (RLine M,l,pD),i = Line M,i by A12, A11, A14, FINSEQ_1:18; :: thesis: verum