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 that
A1: len f = n and
A2: i in Seg n ; :: thesis: mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set KK = the carrier of K;
set C = Matrix_of_Cofactor M;
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 R = RLine (M @ ),i,f;
set LL = LaplaceExpL (RLine (M @ ),i,f),i;
set MCT = mlt TC,Tp;
A3: len (LaplaceExpL (RLine (M @ ),i,f),i) = n by Def7;

A4: now

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

end;

len (mlt TC,Tp) = n by FINSEQ_1:def 18;
hence mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i by A3, A4, FINSEQ_1:18; :: thesis: verum