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 12;

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:92, MATRIX_0:24;

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;

hence mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i) by A3, A4; :: thesis: verum

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 12;

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:92, MATRIX_0:24;

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 :: thesis: for j being Nat st 1 <= j & j <= n holds

(mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . j

len (mlt (TC,Tp)) = n
by CARD_1:def 7;(mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . j

A5:
Indices (M @) = [:(Seg n),(Seg n):]
by MATRIX_0:24;

A6: dom (LaplaceExpL ((RLine ((M @),i,f)),i)) = Seg n by A3, FINSEQ_1:def 3;

A7: width (M @) = n by MATRIX_0:24;

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

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_0:24;

then [j,i] in Indices (Matrix_of_Cofactor M) by A2, A10, ZFMISC_1:87;

then A12: (Matrix_of_Cofactor M) * (j,i) = Cofactor (M,j,i) by Def6;

n = len (Matrix_of_Cofactor M) by MATRIX_0:24;

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_0:def 8;

A14: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

then [i,j] in Indices M by A2, A10, ZFMISC_1:87;

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:61;

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;A6: dom (LaplaceExpL ((RLine ((M @),i,f)),i)) = Seg n by A3, FINSEQ_1:def 3;

A7: width (M @) = n by MATRIX_0:24;

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

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_0:24;

then [j,i] in Indices (Matrix_of_Cofactor M) by A2, A10, ZFMISC_1:87;

then A12: (Matrix_of_Cofactor M) * (j,i) = Cofactor (M,j,i) by Def6;

n = len (Matrix_of_Cofactor M) by MATRIX_0:24;

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_0:def 8;

A14: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

then [i,j] in Indices M by A2, A10, ZFMISC_1:87;

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:61;

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

hence mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i) by A3, A4; :: thesis: verum