let i, j, n be Nat; :: thesis: for K being Field

for M being Matrix of n,K st i in Seg n holds

(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

let K be Field; :: thesis: for M being Matrix of n,K st i in Seg n holds

(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

let M be Matrix of n,K; :: thesis: ( i in Seg n implies (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j)))) )

assume A1: i in Seg n ; :: thesis: (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

set C = Matrix_of_Cofactor M;

len (Matrix_of_Cofactor M) = n by MATRIX_0:24;

then dom (Matrix_of_Cofactor M) = Seg n by FINSEQ_1:def 3;

then A2: Line ((Matrix_of_Cofactor M),i) = Col (((Matrix_of_Cofactor M) @),i) by A1, MATRIX_0:58;

width M = n by MATRIX_0:24;

then A3: len (Line (M,j)) = n by MATRIX_0:def 7;

thus Det (RLine (M,i,(Line (M,j)))) = Sum (LaplaceExpL ((RLine (M,i,(Line (M,j)))),i)) by A1, Th25

.= Sum (mlt ((Col (((Matrix_of_Cofactor M) @),i)),(Line (M,j)))) by A1, A2, A3, Th28

.= (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) by FVSUM_1:64 ; :: thesis: verum

for M being Matrix of n,K st i in Seg n holds

(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

let K be Field; :: thesis: for M being Matrix of n,K st i in Seg n holds

(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

let M be Matrix of n,K; :: thesis: ( i in Seg n implies (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j)))) )

assume A1: i in Seg n ; :: thesis: (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))

set C = Matrix_of_Cofactor M;

len (Matrix_of_Cofactor M) = n by MATRIX_0:24;

then dom (Matrix_of_Cofactor M) = Seg n by FINSEQ_1:def 3;

then A2: Line ((Matrix_of_Cofactor M),i) = Col (((Matrix_of_Cofactor M) @),i) by A1, MATRIX_0:58;

width M = n by MATRIX_0:24;

then A3: len (Line (M,j)) = n by MATRIX_0:def 7;

thus Det (RLine (M,i,(Line (M,j)))) = Sum (LaplaceExpL ((RLine (M,i,(Line (M,j)))),i)) by A1, Th25

.= Sum (mlt ((Col (((Matrix_of_Cofactor M) @),i)),(Line (M,j)))) by A1, A2, A3, Th28

.= (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) by FVSUM_1:64 ; :: thesis: verum