let i, j, n 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_0:24;
width (M @) = n by MATRIX_0:24;
then A4: len (Line ((M @),j)) = n by MATRIX_0:def 7;
A5: width M = n by MATRIX_0:24;
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_0:59
.= (Line (((Matrix_of_Cofactor M) @),i)) "*" (Col (M,j)) by A2, A5, MATRIX_0:59 ; :: thesis: verum