theorem Th15: :: LAPLACE:15

for n being 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)