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 that
A1: i in Seg n and
A2: j in Seg n ; :: thesis: Delete M,i,j = Delete (RLine M,i,f),i,j
A3: Delete M,i,j = Deleting M,i,j by A1, A2, Def1;
A4: Delete (RLine M,i,f),i,j = Deleting (RLine M,i,f),i,j by A1, A2, Def1;
reconsider f' = f as Element of the carrier of K * by FINSEQ_1:def 11;
reconsider I = i as Element of NAT by ORDINAL1:def 13;

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 A3, A4, 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;