theorem Th30: :: LAPLACE:30
for n being Nat
for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n)