let k, l, n, m be Nat; :: thesis: for K being non empty set
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 non empty set ; :: 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_0:def 7;
then A8: width M1 = width M by A5, MATRIX11:def 3;
A9: len qK = width M by A4, MATRIX_0:def 7;
then width M1 = width M2 by A6, A8, MATRIX11:def 3;
hence M2 * (i,j) = (Line (M2,i)) . j by A2, A8, MATRIX_0:def 7
.= qK . j by A1, A6, A7, A9, A8, MATRIX11:28
.= M * (k,j) by A2, A4, MATRIX_0:def 7 ;
:: 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_0:def 7;
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_0:def 7;
then width M1 = width M2 by A6, A12, MATRIX11:def 3;
hence M2 * (i,j) = (Line (M2,i)) . j by A2, A12, MATRIX_0:def 7
.= pK . j by A1, A5, A10, A11, A13, MATRIX11:28
.= M * (l,j) by A2, A3, MATRIX_0:def 7 ;
:: 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_0:def 7;
then A18: width M1 = width M by A5, MATRIX11:def 3;
len qK = len (Line (M,k)) by A4
.= width M by MATRIX_0:def 7 ;
then width M1 = width M2 by A6, A18, MATRIX11:def 3;
hence M2 * (i,j) = (Line (M2,i)) . j by A2, A18, MATRIX_0:def 7
.= (Line (M,i)) . j by A1, A6, A15, A17, MATRIX11:28
.= M * (i,j) by A2, MATRIX_0:def 7 ;
:: thesis: verum

end;