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

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