let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
let K be Field; :: thesis: for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
let M be Matrix of n,K; :: thesis: for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
let f be FinSequence of K; :: thesis: for i being Nat st len f = n & i in Seg n holds
mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
let i be Nat; :: thesis: ( len f = n & i in Seg n implies mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i )
assume A1: ( len f = n & i in Seg n ) ; :: thesis: mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
set C = Matrix_of_Cofactor M;
set KK = the carrier of K;
set R = RLine (M @ ),i,f;
set LL = LaplaceExpL (RLine (M @ ),i,f),i;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
reconsider Tp = f, TC = Col (Matrix_of_Cofactor M),i as Element of N -tuples_on the carrier of K by A1, FINSEQ_2:110, MATRIX_1:25;
set MCT = mlt TC,Tp;
A2: ( len (mlt TC,Tp) = n & len (LaplaceExpL (RLine (M @ ),i,f),i) = n ) by Def7, FINSEQ_1:def 18;

now

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (mlt TC,Tp) . j = (LaplaceExpL (RLine (M @ ),i,f),i) . j )
assume A3: ( 1 <= j & j <= n ) ; :: thesis: (mlt TC,Tp) . j = (LaplaceExpL (RLine (M @ ),i,f),i) . j
j in NAT by ORDINAL1:def 13;
then A4: ( j in Seg n & n = len (Matrix_of_Cofactor M) & width (M @ ) = n & Indices (Matrix_of_Cofactor M) = [:(Seg n),(Seg n):] & Indices M = [:(Seg n),(Seg n):] & Indices (M @ ) = [:(Seg n),(Seg n):] ) by A3, MATRIX_1:25;
then ( Delete (M @ ),i,j = (Delete M,j,i) @ & [j,i] in Indices (Matrix_of_Cofactor M) & [i,j] in Indices M & dom (Matrix_of_Cofactor M) = Seg n ) by A1, Th14, FINSEQ_1:def 3, ZFMISC_1:106;
then ( (Col (Matrix_of_Cofactor M),i) . j = (Matrix_of_Cofactor M) * j,i & (Matrix_of_Cofactor M) * j,i = Cofactor M,j,i & (RLine (M @ ),i,f) * i,j = f . j & Cofactor (RLine (M @ ),i,f),i,j = Cofactor (M @ ),i,j & Cofactor (M @ ),i,j = Cofactor M,j,i & dom (LaplaceExpL (RLine (M @ ),i,f),i) = Seg n ) by A1, A2, A4, Def6, Th15, FINSEQ_1:def 3, MATRIX11:def 3, MATRIXR2:43, MATRIX_1:def 9;
then ( (mlt TC,Tp) . j = (Cofactor M,j,i) * ((RLine (M @ ),i,f) * i,j) & (LaplaceExpL (RLine (M @ ),i,f),i) . j = ((RLine (M @ ),i,f) * i,j) * (Cofactor M,j,i) ) by A4, Def7, FVSUM_1:74;
hence (mlt TC,Tp) . j = (LaplaceExpL (RLine (M @ ),i,f),i) . j ; :: thesis: verum

end;

hence mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i by A2, FINSEQ_1:18; :: thesis: verum