let n be Nat; :: thesis:
let K be Field; :: thesis:
let A be Matrix of n,K; :: thesis:
assume A1: Det A <> 0. K ; :: thesis:
let x, b be FinSequence of K; :: thesis:
assume A2: ( len x = n & A * x = <*b*> @ ) ; :: thesis:
set X = <*x*>;
set B = <*b*>;
len <*x*> = 1 by MATRIX_1:def 3;
then A3: len x = width <*x*> by MATRIX_1:20;
then A4: len (<*x*> @ ) = len x by MATRIX_1:def 7;
hence <*x*> @ = (A ~ ) * b by A1, A2, Th37; :: thesis:
let i be Nat; :: thesis:
assume A5: i in Seg n ; :: thesis:
n <> 0 by A5, FINSEQ_1:4;
then n > 0 ;
then width (<*x*> @ ) = len <*x*> by A2, A3, MATRIX_2:12
.= 1 by MATRIX_1:def 3 ;
then ( Indices (<*x*> @ ) = [:(Seg n),(Seg 1):] & 1 in Seg 1 & len <*b*> = 1 ) by A2, A4, FINSEQ_1:def 3, MATRIX_1:def 3;
then A6: ( [i,1] in Indices (<*x*> @ ) & Line <*x*>,1 = <*x*> . 1 & Line <*b*>,1 = <*b*> . 1 & 1 in dom <*b*> ) by A5, FINSEQ_1:def 3, MATRIX_2:10, ZFMISC_1:106;
then [1,i] in Indices <*x*> by MATRIX_1:def 7;
then (<*x*> @ ) * i,1 = <*x*> * 1,i by MATRIX_1:def 7
.= (Line <*x*>,1) . i by A2, A3, A5, MATRIX_1:def 8
.= x . i by A6, FINSEQ_1:57 ;
hence x . i = ((Det A) " ) * (Det (ReplaceCol A,i,(Col (<*b*> @ ),1))) by A1, A2, A4, A6, Th37
.= ((Det A) " ) * (Det (ReplaceCol A,i,(Line <*b*>,1))) by A6, MATRIX_2:16
.= ((Det A) " ) * (Det (ReplaceCol A,i,b)) by A6, FINSEQ_1:57 ;
:: thesis: