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 A2: ( len x = n & 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*>;
set B = <*b*>;
A3: width <*x*> = len x by MATRIX_1:24;
hence <*x*> = b * (A ~ ) by A1, A2, Th38; :: thesis: for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceLine A,i,b))
let i be Nat; :: thesis: ( i in Seg n implies x . i = ((Det A) " ) * (Det (ReplaceLine A,i,b)) )
assume A4: i in Seg n ; :: thesis: x . i = ((Det A) " ) * (Det (ReplaceLine A,i,b))
1 in Seg 1 ;
then A5: ( [1,i] in [:(Seg 1),(Seg n):] & [:(Seg 1),(Seg n):] = Indices <*x*> & Line <*x*>,1 = <*x*> . 1 & Line <*b*>,1 = <*b*> . 1 ) by A2, A4, MATRIX_1:24, MATRIX_2:10, ZFMISC_1:106;
<*x*> * 1,i = (Line <*x*>,1) . i by A2, A3, A4, MATRIX_1:def 8
.= x . i by A5, FINSEQ_1:57 ;
hence x . i = ((Det A) " ) * (Det (ReplaceLine A,i,(Line <*b*>,1))) by A1, A2, A3, A5, Th38
.= ((Det A) " ) * (Det (ReplaceLine A,i,b)) by A5, FINSEQ_1:57 ;
:: thesis: verum