let k, n, m be Nat; for K being Field
for M being Matrix of n,m,K holds ILine (M,k,k) = M
let K be Field; for M being Matrix of n,m,K holds ILine (M,k,k) = M
let M be Matrix of n,m,K; 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;
( [i,j] in Indices M implies (ILine (M,k,k)) * (i,j) = M * (i,j) )
assume
[i,j] in Indices M
;
(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;
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; verum