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;
set LM = Line M,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 A2: ( i = l & len pD = width M ) ; :: thesis: Line (RLine M,l,pD),i = pD
then A3: width (RLine M,l,pD) = len pD by Def3;
then A4: len (Line (RLine M,l,pD),i) = len pD by MATRIX_1:def 8;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len pD implies (Line (RLine M,l,pD),i) . j = pD . j )
assume A5: ( 1 <= j & j <= len pD ) ; :: thesis: (Line (RLine M,l,pD),i) . j = pD . j
A6: j in NAT by ORDINAL1:def 13;
n = len (RLine M,l,pD) by MATRIX_1:def 3;
then ( j in Seg (width (RLine M,l,pD)) & i in dom (RLine M,l,pD) ) by A1, A3, A5, A6, FINSEQ_1:def 3;
then ( (Line (RLine M,l,pD),i) . j = (RLine M,l,pD) * i,j & [i,j] in Indices (RLine M,l,pD) & Indices (RLine M,l,pD) = Indices M ) by Lm4, MATRIX_1:def 8, ZFMISC_1:106;
hence (Line (RLine M,l,pD),i) . j = pD . j by A2, Def3; :: thesis: verum

end;

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

end;

assume A7: i <> l ; :: thesis: Line (RLine M,l,pD),i = Line M,i
A8: ( len (Line (RLine M,l,pD),i) = width (RLine M,l,pD) & width M = width (RLine M,l,pD) & width M = len (Line M,i) ) by Lm4, MATRIX_1:def 8;

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 A9: ( 1 <= j & j <= len (Line M,i) ) ; :: thesis: (Line M,i) . j = (Line (RLine M,l,pD),i) . j
A10: j in NAT by ORDINAL1:def 13;
i in Seg (len M) by A1, MATRIX_1:def 3;
then ( j in Seg (len (Line M,i)) & i in dom M ) by A9, A10, FINSEQ_1:def 3;
then A11: ( (Line M,i) . j = M * i,j & (Line (RLine M,l,pD),i) . j = (RLine M,l,pD) * i,j & [i,j] in Indices M ) by A8, MATRIX_1:def 8, ZFMISC_1:106;

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 A7, A11, 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;

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