let l, k, n, m be Nat; :: thesis: for K being Field
for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(ILine M1,l,k) @ = ICol M,l,k
let K be Field; :: thesis: for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds
(ILine M1,l,k) @ = ICol M,l,k
let M, M1 be Matrix of n,m,K; :: thesis: ( l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ implies (ILine M1,l,k) @ = ICol M,l,k )
assume A1: ( l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ ) ; :: thesis: (ILine M1,l,k) @ = ICol M,l,k
then ( len M = n & width M = m ) by MATRIX_1:24;
then A2: ( len M1 = m & width M1 = n ) by A1, MATRIX_2:12;
( len (ILine M1,l,k) = len M1 & width (ILine M1,l,k) = width M1 ) by Def1, Th1;
then ( len ((ILine M1,l,k) @ ) = n & width ((ILine M1,l,k) @ ) = m ) by A1, A2, MATRIX_2:12;
then A3: (ILine M1,l,k) @ is Matrix of n,m,K by A1, MATRIX_1:20;
then consider M2 being Matrix of n,m,K such that
A4: M2 = (ILine M1,l,k) @ ;
A5: 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 A6: ( i in dom M & 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 ) )
then A7: [i,j] in Indices M by ZFMISC_1:106;
then A8: [j,i] in Indices M1 by A1, MATRIX_1:def 7;
then A9: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:106;
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 A10: [j,i] in Indices (ILine M1,l,k) by A8, 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

assume A11: j = l ; :: thesis: M2 * i,j = M * i,k
A12: [i,k] in Indices M by A1, A6, ZFMISC_1:106;
M2 * i,j = (ILine M1,l,k) * j,i by A4, A10, MATRIX_1:def 7
.= M1 * k,i by A9, A11, Def1
.= M * i,k by A1, A12, MATRIX_1:def 7 ;
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

assume A13: j = k ; :: thesis: M2 * i,j = M * i,l
A14: [i,l] in Indices M by A1, A6, ZFMISC_1:106;
M2 * i,j = (ILine M1,l,k) * j,i by A4, A10, MATRIX_1:def 7
.= M1 * l,i by A9, A13, Def1
.= M * i,l by A1, A14, MATRIX_1:def 7 ;
hence M2 * i,j = M * i,l ; :: thesis: verum

end;

assume A15: ( j <> l & j <> k ) ; :: thesis: M2 * i,j = M * i,j
M2 * i,j = (ILine M1,l,k) * j,i by A4, A10, MATRIX_1:def 7
.= M1 * j,i by A9, A15, Def1
.= M * i,j by A1, A7, MATRIX_1:def 7 ;
hence M2 * i,j = M * i,j ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (ICol M,l,k) holds
(ICol M,l,k) * i,j = ((ILine M1,l,k) @ ) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ICol M,l,k) implies (ICol M,l,k) * i,j = ((ILine M1,l,k) @ ) * i,j )
assume A16: [i,j] in Indices (ICol M,l,k) ; :: thesis: (ICol M,l,k) * i,j = ((ILine M1,l,k) @ ) * i,j
( Indices (ICol M,l,k) = Indices ((ILine M1,l,k) @ ) & Indices M = Indices (ICol M,l,k) ) by A4, MATRIX_1:27;
then ( i in dom M & j in Seg (width M) ) by A16, ZFMISC_1:106;
then ( ( j = l implies ((ILine M1,l,k) @ ) * i,j = M * i,k ) & ( j = k implies ((ILine M1,l,k) @ ) * i,j = M * i,l ) & ( j <> l & j <> k implies ((ILine M1,l,k) @ ) * i,j = M * i,j ) & ( j = l implies (ICol M,l,k) * i,j = M * i,k ) & ( j = k implies (ICol M,l,k) * i,j = M * i,l ) & ( j <> l & j <> k implies (ICol M,l,k) * i,j = M * i,j ) ) by A1, A4, A5, Def4;
hence (ICol M,l,k) * i,j = ((ILine M1,l,k) @ ) * i,j ; :: thesis: verum

end;

hence (ILine M1,l,k) @ = ICol M,l,k by A3, MATRIX_1:28; :: thesis: verum