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 f9 = f as Element of the carrier of K * by FINSEQ_1:def 11;
reconsider I = i as Element of NAT by ORDINAL1:def 12;

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,f9) by MATRIX11:29;
hence Delete (M,i,j) = Delete ((RLine (M,i,f)),i,j) by A3, A4, COMPUT_1:3; :: 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;