theorem Th38: :: LAPLACE:38

for n being Nat
for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being Matrix of K st width x = n & x * A = b holds
( x = b * (A ~) & ( for i, j being Nat st [i,j] in Indices x holds
x * (i,j) = ((Det A) ") * (Det (ReplaceLine (A,j,(Line (b,i))))) ) )