let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let k, l be Nat; :: thesis:
let M, M1, M2 be Matrix of n,m,K; :: thesis:
let pK, qK be FinSequence of K; :: thesis:
let i, j be Nat; :: thesis:
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:
thus ( i = l implies M2 * (i,j) = M * (k,j) ) :: thesis:

proof

assume A7: i = l ; :: thesis:
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:

end;

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

proof

assume A10: i = k ; :: thesis:
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:

per cases ;

suppose l <> k ; :: thesis:

hence Line (M2,i) = Line (M1,i) by A1, A6, A14, MATRIX11:28; :: thesis:

end;

suppose l = k ; :: thesis:

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:

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:

end;

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

proof

assume that
A15: i <> l and
A16: i <> k ; :: thesis:
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 = width M by A4, 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:

end;