for i, j, n being Nat
for K being Field
for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)