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 & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (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 & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (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 & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) ) )

assume A1: Det A <> 0. K ; :: thesis: for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) )

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

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) ) )

assume that

A2: len x = n and

A3: A * x = <*b*> @ ; :: thesis: ( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) )

set X = <*x*>;

len <*x*> = 1 by MATRIX_0:def 2;

then A4: len x = width <*x*> by MATRIX_0:20;

then A5: len (<*x*> @) = len x by MATRIX_0:def 6;

hence <*x*> @ = (A ~) * b by A1, A2, A3, Th37; :: thesis: for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b)))

set B = <*b*>;

A6: 1 in Seg 1 ;

then A7: Line (<*x*>,1) = <*x*> . 1 by MATRIX_0:52;

len <*b*> = 1 by MATRIX_0:def 2;

then A8: 1 in dom <*b*> by A6, FINSEQ_1:def 3;

A9: Line (<*b*>,1) = <*b*> . 1 by A6, MATRIX_0:52;

let i be Nat; :: thesis: ( i in Seg n implies x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) )

assume A10: i in Seg n ; :: thesis: x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b)))

n > 0 by A10;

then width (<*x*> @) = len <*x*> by A2, A4, MATRIX_0:54

.= 1 by MATRIX_0:def 2 ;

then Indices (<*x*> @) = [:(Seg n),(Seg 1):] by A2, A5, FINSEQ_1:def 3;

then A11: [i,1] in Indices (<*x*> @) by A10, A6, ZFMISC_1:87;

then [1,i] in Indices <*x*> by MATRIX_0:def 6;

then (<*x*> @) * (i,1) = <*x*> * (1,i) by MATRIX_0:def 6

.= (Line (<*x*>,1)) . i by A2, A4, A10, MATRIX_0:def 7

.= x . i by A7, FINSEQ_1:40 ;

hence x . i = ((Det A) ") * (Det (ReplaceCol (A,i,(Col ((<*b*> @),1))))) by A1, A2, A3, A5, A11, Th37

.= ((Det A) ") * (Det (ReplaceCol (A,i,(Line (<*b*>,1))))) by A8, MATRIX_0:58

.= ((Det A) ") * (Det (ReplaceCol (A,i,b))) by A9, FINSEQ_1:40 ;

:: thesis: verum

for A being Matrix of n,K st Det A <> 0. K holds

for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (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 & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (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 & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) ) )

assume A1: Det A <> 0. K ; :: thesis: for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds

( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) )

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

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) ) )

assume that

A2: len x = n and

A3: A * x = <*b*> @ ; :: thesis: ( <*x*> @ = (A ~) * b & ( for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) ) )

set X = <*x*>;

len <*x*> = 1 by MATRIX_0:def 2;

then A4: len x = width <*x*> by MATRIX_0:20;

then A5: len (<*x*> @) = len x by MATRIX_0:def 6;

hence <*x*> @ = (A ~) * b by A1, A2, A3, Th37; :: thesis: for i being Nat st i in Seg n holds

x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b)))

set B = <*b*>;

A6: 1 in Seg 1 ;

then A7: Line (<*x*>,1) = <*x*> . 1 by MATRIX_0:52;

len <*b*> = 1 by MATRIX_0:def 2;

then A8: 1 in dom <*b*> by A6, FINSEQ_1:def 3;

A9: Line (<*b*>,1) = <*b*> . 1 by A6, MATRIX_0:52;

let i be Nat; :: thesis: ( i in Seg n implies x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b))) )

assume A10: i in Seg n ; :: thesis: x . i = ((Det A) ") * (Det (ReplaceCol (A,i,b)))

n > 0 by A10;

then width (<*x*> @) = len <*x*> by A2, A4, MATRIX_0:54

.= 1 by MATRIX_0:def 2 ;

then Indices (<*x*> @) = [:(Seg n),(Seg 1):] by A2, A5, FINSEQ_1:def 3;

then A11: [i,1] in Indices (<*x*> @) by A10, A6, ZFMISC_1:87;

then [1,i] in Indices <*x*> by MATRIX_0:def 6;

then (<*x*> @) * (i,1) = <*x*> * (1,i) by MATRIX_0:def 6

.= (Line (<*x*>,1)) . i by A2, A4, A10, MATRIX_0:def 7

.= x . i by A7, FINSEQ_1:40 ;

hence x . i = ((Det A) ") * (Det (ReplaceCol (A,i,(Col ((<*b*> @),1))))) by A1, A2, A3, A5, A11, Th37

.= ((Det A) ") * (Det (ReplaceCol (A,i,(Line (<*b*>,1))))) by A8, MATRIX_0:58

.= ((Det A) ") * (Det (ReplaceCol (A,i,b))) by A9, FINSEQ_1:40 ;

:: thesis: verum