let k, l, n, m be Nat; :: thesis: for K being comRing
for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)
let K be comRing; :: thesis: for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)
let M be Matrix of n,m,K; :: thesis: ILine (M,l,k) = ILine (M,k,l)
A1: width (ILine (M,k,l)) = width M by Th1;
A2: for i, j being Nat st [i,j] in Indices (ILine (M,l,k)) holds
(ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ILine (M,l,k)) implies (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) )
A3: Indices (ILine (M,l,k)) = Indices M by MATRIX_0:26;
assume [i,j] in Indices (ILine (M,l,k)) ; :: thesis: (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j)
then A4: ( i in dom M & j in Seg (width M) ) by A3, ZFMISC_1:87;
then A5: ( i = k implies (ILine (M,l,k)) * (i,j) = M * (l,j) ) by Def1;
A6: ( i = l implies (ILine (M,k,l)) * (i,j) = M * (k,j) ) by A4, Def1;
A7: ( i <> l & i <> k implies (ILine (M,l,k)) * (i,j) = M * (i,j) ) by A4, Def1;
A8: ( i = k implies (ILine (M,k,l)) * (i,j) = M * (l,j) ) by A4, Def1;
( i = l implies (ILine (M,l,k)) * (i,j) = M * (k,j) ) by A4, Def1;
hence (ILine (M,l,k)) * (i,j) = (ILine (M,k,l)) * (i,j) by A4, A5, A7, A6, A8, Def1; :: thesis: verum

end;

( len (ILine (M,l,k)) = len M & len (ILine (M,k,l)) = len M ) by Def1;
hence ILine (M,l,k) = ILine (M,k,l) by A1, A2, Th1, MATRIX_0:21; :: thesis: verum