let n, m, l, k be Nat; :: thesis: for K being Field
for M being Matrix of n,m,K holds ILine M,l,k = ILine M,k,l
let K be Field; :: 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_1:27;
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:106;
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_1:21; :: thesis: verum