let n be Nat; :: thesis: 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))) ) )

let K be Field; :: thesis: 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))) ) )

let A be Matrix of n,K; :: thesis: ( Det A <> 0. K implies 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))) ) ) )

assume A1: Det A <> 0. K ; :: thesis: 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))) ) )

let x, b be FinSequence of K; :: thesis: ( len x = n & x * A = <*b*> implies ( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) ) )

assume that
A2: len x = n and
A3: x * A = <*b*> ; :: thesis: ( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) )

set X = <*x*>;
A4: width <*x*> = len x by MATRIX_0:23;
hence <*x*> = b * (A ~) by A1, A2, A3, Th38; :: thesis: for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b)))

A5: [:(Seg 1),(Seg n):] = Indices <*x*> by ;
set B = <*b*>;
A6: 1 in Seg 1 ;
then A7: Line (<*x*>,1) = <*x*> . 1 by MATRIX_0:52;
let i be Nat; :: thesis: ( i in Seg n implies x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) )
assume A8: i in Seg n ; :: thesis: x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b)))
A9: [1,i] in [:(Seg 1),(Seg n):] by ;
A10: Line (<*b*>,1) = <*b*> . 1 by ;
<*x*> * (1,i) = (Line (<*x*>,1)) . i by
.= x . i by ;
hence x . i = ((Det A) ") * (Det (ReplaceLine (A,i,(Line (<*b*>,1))))) by A1, A2, A3, A4, A9, A5, Th38
.= ((Det A) ") * (Det (ReplaceLine (A,i,b))) by ;
:: thesis: verum