theorem Th31: :: LAPLACE:31

for n being Nat
for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)