let m, n be Nat; :: thesis: for K being Field
for k, l being Nat
for M, M1, M2 being Matrix of n,m,K
for pK, qK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
let K be Field; :: thesis: for k, l being Nat
for M, M1, M2 being Matrix of n,m,K
for pK, qK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
let k, l be Nat; :: thesis: for M, M1, M2 being Matrix of n,m,K
for pK, qK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
let M, M1, M2 be Matrix of n,m,K; :: thesis: for pK, qK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
let pK, qK be FinSequence of K; :: thesis: for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK holds
( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK implies ( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) ) )
assume A1: ( i in Seg n & j in Seg (width M) & pK = Line M,l & qK = Line M,k & M1 = RLine M,k,pK & M2 = RLine M1,l,qK ) ; :: thesis: ( ( i = l implies M2 * i,j = M * k,j ) & ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )
thus ( i = l implies M2 * i,j = M * k,j ) :: thesis: ( ( i = k implies M2 * i,j = M * l,j ) & ( i <> l & i <> k implies M2 * i,j = M * i,j ) )

proof

assume A2: i = l ; :: thesis: M2 * i,j = M * k,j
A3: ( len pK = width M & len qK = width M ) by A1, MATRIX_1:def 8;
then A4: width M1 = width M by A1, MATRIX11:def 3;
then width M1 = width M2 by A1, A3, MATRIX11:def 3;
hence M2 * i,j = (Line M2,i) . j by A1, A4, MATRIX_1:def 8
.= qK . j by A1, A2, A3, A4, MATRIX11:28
.= M * k,j by A1, MATRIX_1:def 8 ;
:: thesis: verum

end;

thus ( i = k implies M2 * i,j = M * l,j ) :: thesis: ( i <> l & i <> k implies M2 * i,j = M * i,j )

proof

assume A5: i = k ; :: thesis: M2 * i,j = M * l,j
A6: ( len pK = width M & len qK = width M ) by A1, MATRIX_1:def 8;
then A7: width M1 = width M by A1, MATRIX11:def 3;
then A8: width M1 = width M2 by A1, A6, MATRIX11:def 3;
A9: ( i = k implies Line M2,i = Line M1,i )

proof

assume A10: i = k ; :: thesis: Line M2,i = Line M1,i

per cases ( l <> k or l = k ) ;

suppose l <> k ; :: thesis: Line M2,i = Line M1,i

hence Line M2,i = Line M1,i by A1, A10, MATRIX11:28; :: thesis: verum

end;

suppose l = k ; :: thesis: Line M2,i = Line M1,i

then Line M2,i = pK by A1, A5, A6, A7, MATRIX11:28;
hence Line M2,i = Line M1,i by A1, A5, A6, MATRIX11:28; :: thesis: verum

end;

end;

end;

thus M2 * i,j = (Line M2,i) . j by A1, A7, A8, MATRIX_1:def 8
.= pK . j by A1, A5, A6, A9, MATRIX11:28
.= M * l,j by A1, MATRIX_1:def 8 ; :: thesis: verum

end;

thus ( i <> l & i <> k implies M2 * i,j = M * i,j ) :: thesis: verum

proof

assume A11: ( i <> l & i <> k ) ; :: thesis: M2 * i,j = M * i,j
A12: ( len pK = width M & len qK = width M ) by A1, MATRIX_1:def 8;
then A13: width M1 = width M by A1, MATRIX11:def 3;
then A14: width M1 = width M2 by A1, A12, MATRIX11:def 3;
A15: Line M1,i = Line M,i by A1, A11, MATRIX11:28;
thus M2 * i,j = (Line M2,i) . j by A1, A13, A14, MATRIX_1:def 8
.= (Line M,i) . j by A1, A11, A15, MATRIX11:28
.= M * i,j by A1, MATRIX_1:def 8 ; :: thesis: verum

end;