let k, l, n, m be Nat; :: thesis: for K being comRing
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 comRing; :: 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 that
A1: l in Seg (width M) and
A2: k in Seg (width M) and
A3: n > 0 and
A4: m > 0 and
A5: M1 = M @ ; :: thesis: (ILine (M1,l,k)) @ = ICol (M,l,k)
A6: width M = m by A3, MATRIX_0:23;
A7: width (ILine (M1,l,k)) = width M1 by Th1;
len M = n by A3, MATRIX_0:23;
then A8: width M1 = n by A4, A5, A6, MATRIX_0:54;
then A9: len ((ILine (M1,l,k)) @) = n by A3, A7, MATRIX_0:54;
A10: len (ILine (M1,l,k)) = len M1 by Def1;
len M1 = m by A4, A5, A6, MATRIX_0:54;
then width ((ILine (M1,l,k)) @) = m by A3, A8, A10, A7, MATRIX_0:54;
then A11: (ILine (M1,l,k)) @ is Matrix of n,m,K by A3, A9, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A12: M2 = (ILine (M1,l,k)) @ ;
A13: 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
A14: i in dom M and
A15: 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) ) )
A16: [i,j] in Indices M by A14, A15, ZFMISC_1:87;
then A17: [j,i] in Indices M1 by A5, MATRIX_0:def 6;
then A18: ( 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 A19: [j,i] in Indices (ILine (M1,l,k)) by A17, 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

A20: [i,k] in Indices M by A2, A14, ZFMISC_1:87;
assume A21: j = l ; :: thesis: M2 * (i,j) = M * (i,k)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_0:def 6
.= M1 * (k,i) by A18, A21, Def1
.= M * (i,k) by A5, A20, 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

A22: [i,l] in Indices M by A1, A14, ZFMISC_1:87;
assume A23: j = k ; :: thesis: M2 * (i,j) = M * (i,l)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_0:def 6
.= M1 * (l,i) by A18, A23, Def1
.= M * (i,l) by A5, A22, MATRIX_0:def 6 ;
hence M2 * (i,j) = M * (i,l) ; :: thesis: verum

end;

assume A24: ( j <> l & j <> k ) ; :: thesis: M2 * (i,j) = M * (i,j)
M2 * (i,j) = (ILine (M1,l,k)) * (j,i) by A12, A19, MATRIX_0:def 6
.= M1 * (j,i) by A18, A24, Def1
.= M * (i,j) by A5, A16, MATRIX_0:def 6 ;
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

A25: Indices M = Indices (ICol (M,l,k)) by MATRIX_0:26;
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 [i,j] in Indices (ICol (M,l,k)) ; :: thesis: (ICol (M,l,k)) * (i,j) = ((ILine (M1,l,k)) @) * (i,j)
then A26: ( i in dom M & j in Seg (width M) ) by A25, ZFMISC_1:87;
then A27: ( j = l implies ((ILine (M1,l,k)) @) * (i,j) = M * (i,k) ) by A12, A13;
A28: ( j = k implies (ICol (M,l,k)) * (i,j) = M * (i,l) ) by A1, A3, A4, A26, Def4;
A29: ( j = k implies ((ILine (M1,l,k)) @) * (i,j) = M * (i,l) ) by A12, A13, A26;
A30: ( j <> l & j <> k implies ((ILine (M1,l,k)) @) * (i,j) = M * (i,j) ) by A12, A13, A26;
( j = l implies (ICol (M,l,k)) * (i,j) = M * (i,k) ) by A2, A3, A4, A26, Def4;
hence (ICol (M,l,k)) * (i,j) = ((ILine (M1,l,k)) @) * (i,j) by A1, A2, A3, A4, A26, A27, A29, A30, A28, Def4; :: thesis: verum

end;

hence (ILine (M1,l,k)) @ = ICol (M,l,k) by A11, MATRIX_0:27; :: thesis: verum