let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg n holds
Delete M,i,j = Delete (RLine M,i,f),i,j
let K be Field; :: thesis: for M being Matrix of n,K
for f being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg n holds
Delete M,i,j = Delete (RLine M,i,f),i,j
let M be Matrix of n,K; :: thesis: for f being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg n holds
Delete M,i,j = Delete (RLine M,i,f),i,j
let f be FinSequence of K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n holds
Delete M,i,j = Delete (RLine M,i,f),i,j
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n implies Delete M,i,j = Delete (RLine M,i,f),i,j )
assume A1: ( i in Seg n & j in Seg n ) ; :: thesis: Delete M,i,j = Delete (RLine M,i,f),i,j
reconsider I = i as Element of NAT by ORDINAL1:def 13;
A2: ( Delete M,i,j = Deleting M,i,j & Deleting M,i,j = DelCol (DelLine M,i),j & Delete (RLine M,i,f),i,j = Deleting (RLine M,i,f),i,j & Deleting (RLine M,i,f),i,j = DelCol (DelLine (RLine M,i,f),i),j ) by A1, Def1;
reconsider f' = f as Element of the carrier of K * by FINSEQ_1:def 11;

per cases ( len f = width M or len f <> width M ) ;

suppose len f = width M ; :: thesis: Delete M,i,j = Delete (RLine M,i,f),i,j

then RLine M,I,f = Replace M,i,f' by MATRIX11:29;
hence Delete M,i,j = Delete (RLine M,i,f),i,j by A2, COMPUT_1:6; :: thesis: verum

end;

suppose len f <> width M ; :: thesis: Delete M,i,j = Delete (RLine M,i,f),i,j

hence Delete M,i,j = Delete (RLine M,i,f),i,j by MATRIX11:def 3; :: thesis: verum

end;

end;