for n being Nat
for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )