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 ((),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 ((),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 ((),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 ((),i)) "*" (Col (M,j)) = Det (RLine ((M @),i,(Line ((M @),j))))
set C = Matrix_of_Cofactor M;
set L = Line ((M @),j);
A3: width = 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
.= Sum (mlt ((Col (,i)),(Line ((M @),j)))) by A1, A4, Th31
.= (Line ((),i)) "*" (Line ((M @),j)) by
.= (Line ((),i)) "*" (Col (M,j)) by ; :: thesis: verum