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;

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 )
;

end;

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