let n, m, l, k be Nat; :: thesis: for K being Field
for M being Matrix of n,m,K st l in dom M & k in dom M holds
ILine (ILine M,l,k),l,k = M
let K be Field; :: thesis: for M being Matrix of n,m,K st l in dom M & k in dom M holds
ILine (ILine M,l,k),l,k = M
let M be Matrix of n,m,K; :: thesis: ( l in dom M & k in dom M implies ILine (ILine M,l,k),l,k = M )
assume A1: ( l in dom M & k in dom M ) ; :: thesis: ILine (ILine M,l,k),l,k = M
set M1 = ILine M,l,k;
A2: ( len (ILine M,l,k) = len M & width (ILine M,l,k) = width M ) by Def1, Th1;
A3: dom (ILine M,l,k) = Seg (len (ILine M,l,k)) by FINSEQ_1:def 3
.= Seg (len M) by Def1
.= dom M by FINSEQ_1:def 3 ;
A4: ( len (ILine (ILine M,l,k),l,k) = len (ILine M,l,k) & width (ILine (ILine M,l,k),l,k) = width (ILine M,l,k) ) by Def1, Th1;
for i, j being Nat st [i,j] in Indices M holds
(ILine (ILine M,l,k),l,k) * i,j = M * i,j

proof

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

end;

hence ILine (ILine M,l,k),l,k = M by A2, A4, MATRIX_1:21; :: thesis: verum