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

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies (ILine (M,k,k)) * (i,j) = M * (i,j) )
assume [i,j] in Indices M ; :: thesis: (ILine (M,k,k)) * (i,j) = M * (i,j)
then A2: ( i in dom M & j in Seg (width M) ) by ZFMISC_1:87;
then ( i = k implies (ILine (M,k,k)) * (i,j) = M * (k,j) ) by Def1;
hence (ILine (M,k,k)) * (i,j) = M * (i,j) by A2, Def1; :: thesis: verum

end;

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