A5: width M = m by A3, MATRIX_0:23;
then A6: len (M @) = m by A4, MATRIX_0:54;
A7: len M = n by A3, MATRIX_0:23;
then width (M @) = n by A4, A5, MATRIX_0:54;
then M @ is Matrix of m,n,K by A4, A6, MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A8: M1 = M @ ;
A9: width (ILine (M1,l,k)) = n by A4, MATRIX_0:23;
then A10: len ((ILine (M1,l,k)) @) = n by A3, MATRIX_0:54;
len (ILine (M1,l,k)) = m by A4, MATRIX_0:23;
then width ((ILine (M1,l,k)) @) = m by A3, A9, MATRIX_0:54;
then (ILine (M1,l,k)) @ is Matrix of n,m,K by A3, A10, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11: M2 = (ILine (M1,l,k)) @ ;
take M2 ; :: thesis: ( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) ) )
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) )

proof

let i, j be Nat; :: thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) )
assume that
A12: i in dom M and
A13: j in Seg (width M) ; :: thesis: ( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) )
A14: [i,j] in Indices M by A12, A13, ZFMISC_1:87;
then A15: [j,i] in Indices M1 by A8, MATRIX_0:def 6;
then A16: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:87;
dom (ILine (M1,l,k)) = Seg (len (ILine (M1,l,k))) by FINSEQ_1:def 3
.= Seg (len M1) by Def1
.= dom M1 by FINSEQ_1:def 3 ;
then A17: [j,i] in Indices (ILine (M1,l,k)) by A15, Th1;
thus ( j = l implies M2 * (i,j) = M * (i,k) ) :: thesis: ( ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) )

proof

A18: [i,k] in Indices M by A2, A12, ZFMISC_1:87;
assume A19: j = l ; :: thesis: M2 * (i,j) = M * (i,k)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_0:def 6
.= M1 * (k,i) by A16, A19, Def1
.= M * (i,k) by A8, A18, MATRIX_0:def 6 ;
hence M2 * (i,j) = M * (i,k) ; :: thesis: verum

end;

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

proof

A20: [i,l] in Indices M by A1, A12, ZFMISC_1:87;
assume A21: j = k ; :: thesis: M2 * (i,j) = M * (i,l)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_0:def 6
.= M1 * (l,i) by A16, A21, Def1
.= M * (i,l) by A8, A20, MATRIX_0:def 6 ;
hence M2 * (i,j) = M * (i,l) ; :: thesis: verum

end;

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

proof

assume A22: ( j <> l & j <> k ) ; :: thesis: M2 * (i,j) = M * (i,j)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A11, A17, MATRIX_0:def 6
.= M1 * (j,i) by A16, A22, Def1
.= M * (i,j) by A8, A14, MATRIX_0:def 6 ;
hence M2 * (i,j) = M * (i,j) ; :: thesis: verum

end;

end;

hence ( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = M * (i,k) ) & ( j = k implies M2 * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies M2 * (i,j) = M * (i,j) ) ) ) ) by A3, A7, MATRIX_0:23; :: thesis: verum