let n be Nat; 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; 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; 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; 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; ( 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
; 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
;
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;
verum end;