let n be Nat; :: thesis: for K being Field
for f being FinSequence of K
for M being Matrix of n,K
for p being Element of Permutations n
for i being Nat st len f = n & i in Seg n holds
mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i)

let K be Field; :: thesis: for f being FinSequence of K
for M being Matrix of n,K
for p being Element of Permutations n
for i being Nat st len f = n & i in Seg n holds
mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i)

let f be FinSequence of K; :: thesis: for M being Matrix of n,K
for p being Element of Permutations n
for i being Nat st len f = n & i in Seg n holds
mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i)

let M be Matrix of n,K; :: thesis: for p being Element of Permutations n
for i being Nat st len f = n & i in Seg n holds
mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i)

let p be Element of Permutations n; :: thesis: for i being Nat st len f = n & i in Seg n holds
mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i)

let i be Nat; :: thesis: ( len f = n & i in Seg n implies mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i) )
assume that
A1: len f = n and
A2: i in Seg n ; :: thesis: mlt ((Line (,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, TL = Line (,i) as Element of N -tuples_on the carrier of K by ;
set R = RLine (M,i,f);
set LL = LaplaceExpL ((RLine (M,i,f)),i);
set MLT = mlt (TL,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 (TL,Tp)) . j = (LaplaceExpL ((RLine (M,i,f)),i)) . j
A5: dom (LaplaceExpL ((RLine (M,i,f)),i)) = Seg n by ;
A6: n = width M by MATRIX_0:24;
let j be Nat; :: thesis: ( 1 <= j & j <= n implies (mlt (TL,Tp)) . j = (LaplaceExpL ((RLine (M,i,f)),i)) . j )
assume that
A7: 1 <= j and
A8: j <= n ; :: thesis: (mlt (TL,Tp)) . j = (LaplaceExpL ((RLine (M,i,f)),i)) . j
A9: j in Seg n by A7, A8;
n = width by MATRIX_0:24;
then A10: (Line (,i)) . j = * (i,j) by ;
Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
then [i,j] in Indices M by ;
then A11: (RLine (M,i,f)) * (i,j) = f . j by ;
Indices = [:(Seg n),(Seg n):] by MATRIX_0:24;
then [i,j] in Indices by ;
then (Line (,i)) . j = Cofactor (M,i,j) by ;
then A12: (mlt (TL,Tp)) . j = (Cofactor (M,i,j)) * ((RLine (M,i,f)) * (i,j)) by ;
Cofactor (M,i,j) = Cofactor ((RLine (M,i,f)),i,j) by A2, A9, Th15;
hence (mlt (TL,Tp)) . j = (LaplaceExpL ((RLine (M,i,f)),i)) . j by A9, A5, A12, Def7; :: thesis: verum
end;
len (mlt (TL,Tp)) = n by CARD_1:def 7;
hence mlt ((Line (,i)),f) = LaplaceExpL ((RLine (M,i,f)),i) by A3, A4; :: thesis: verum