let k, l, n, m be Nat; :: thesis: for K being comRing
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 comRing; :: 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:87;
A7: i in dom M by A5, ZFMISC_1:87;
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_0:21; :: thesis: verum