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 that
A1: i in Seg n and
A2: j in Seg (width M) and
A3: pK = Line M,l and
A4: qK = Line M,k and
A5: M1 = RLine M,k,pK and
A6: 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 A7: i = l ; :: thesis: M2 * i,j = M * k,j
len pK = width M by A3, MATRIX_1:def 8;
then A8: width M1 = width M by A5, MATRIX11:def 3;
A9: len qK = width M by A4, MATRIX_1:def 8;
then width M1 = width M2 by A6, A8, MATRIX11:def 3;
hence M2 * i,j = (Line M2,i) . j by A2, A8, MATRIX_1:def 8
.= qK . j by A1, A6, A7, A9, A8, MATRIX11:28
.= M * k,j by A2, A4, 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 A10: i = k ; :: thesis: M2 * i,j = M * l,j
A11: len pK = width M by A3, MATRIX_1:def 8;
then A12: width M1 = width M by A5, MATRIX11:def 3;
A13: ( i = k implies Line M2,i = Line M1,i )

proof

assume A14: 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, A6, A14, MATRIX11:28; :: thesis: verum

end;

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

then Line M2,i = pK by A1, A3, A4, A6, A10, A11, A12, MATRIX11:28;
hence Line M2,i = Line M1,i by A1, A5, A10, A11, MATRIX11:28; :: thesis: verum

end;

end;

end;

len qK = width M by A4, MATRIX_1:def 8;
then width M1 = width M2 by A6, A12, MATRIX11:def 3;
hence M2 * i,j = (Line M2,i) . j by A2, A12, MATRIX_1:def 8
.= pK . j by A1, A5, A10, A11, A13, MATRIX11:28
.= M * l,j by A2, A3, MATRIX_1:def 8 ;
:: thesis: verum

end;

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

proof

assume that
A15: i <> l and
A16: i <> k ; :: thesis: M2 * i,j = M * i,j
A17: Line M1,i = Line M,i by A1, A5, A16, MATRIX11:28;
len pK = width M by A3, MATRIX_1:def 8;
then A18: width M1 = width M by A5, MATRIX11:def 3;
len qK = width M by A4, MATRIX_1:def 8;
then width M1 = width M2 by A6, A18, MATRIX11:def 3;
hence M2 * i,j = (Line M2,i) . j by A2, A18, MATRIX_1:def 8
.= (Line M,i) . j by A1, A6, A15, A17, MATRIX11:28
.= M * i,j by A2, MATRIX_1:def 8 ;
:: thesis: verum

end;