let i, n, j be Nat; :: thesis: for K being Field
for M being Matrix of n,K st i in Seg n & j in Seg n holds
(Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) = Det (RLine (M @ ),i,(Line (M @ ),j))
let K be Field; :: thesis: for M being Matrix of n,K st i in Seg n & j in Seg n holds
(Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) = Det (RLine (M @ ),i,(Line (M @ ),j))
let M be Matrix of n,K; :: thesis: ( i in Seg n & j in Seg n implies (Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) = Det (RLine (M @ ),i,(Line (M @ ),j)) )
assume that
A1: i in Seg n and
A2: j in Seg n ; :: thesis: (Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) = Det (RLine (M @ ),i,(Line (M @ ),j))
set C = Matrix_of_Cofactor M;
set L = Line (M @ ),j;
A3: width (Matrix_of_Cofactor M) = n by MATRIX_1:25;
width (M @ ) = n by MATRIX_1:25;
then A4: len (Line (M @ ),j) = n by MATRIX_1:def 8;
A5: width M = n by MATRIX_1:25;
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, A4, Th31
.= (Line ((Matrix_of_Cofactor M) @ ),i) "*" (Line (M @ ),j) by A1, A3, MATRIX_2:17
.= (Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) by A2, A5, MATRIX_2:17 ; :: thesis: verum