theorem :: LAPLACE:40

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 FinSequence of K st len x = n & x * A = <*b*> holds
( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) )