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: 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 ;
A3: width (ILine M,l,k) = width M by Th1;
A4: 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 A5: [i,j] in Indices M ; :: thesis: (ILine (ILine M,l,k),l,k) * i,j = M * i,j
then A6: j in Seg (width M) by ZFMISC_1:106;
A7: i in dom M by A5, ZFMISC_1:106;
then ( i <> l & i <> k implies (ILine (ILine M,l,k),l,k) * i,j = (ILine M,l,k) * i,j ) by A3, A2, A6, Def1;
then A8: ( i <> l & i <> k implies (ILine (ILine M,l,k),l,k) * i,j = M * i,j ) by A7, A6, Def1;
( (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 ) by A1, A3, A2, A6, Def1;
hence (ILine (ILine M,l,k),l,k) * i,j = M * i,j by A1, A6, A8, Def1; :: thesis: verum

end;

A9: width (ILine (ILine M,l,k),l,k) = width (ILine M,l,k) by Th1;
( len (ILine M,l,k) = len M & len (ILine (ILine M,l,k),l,k) = len (ILine M,l,k) ) by Def1;
hence ILine (ILine M,l,k),l,k = M by A9, A4, Th1, MATRIX_1:21; :: thesis: verum