let i, n, j 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_1:25;
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_2:16;
width M = n by MATRIX_1:25;
then A3: len (Line M,j) = n by MATRIX_1:def 8;
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:78 ; :: thesis: verum