let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for i being Nat st i in Seg n holds
LaplaceExpC M,i = LaplaceExpL (M @ ),i
let K be Field; :: thesis: for M being Matrix of n,K
for i being Nat st i in Seg n holds
LaplaceExpC M,i = LaplaceExpL (M @ ),i
let M be Matrix of n,K; :: thesis: for i being Nat st i in Seg n holds
LaplaceExpC M,i = LaplaceExpL (M @ ),i
let i be Nat; :: thesis: ( i in Seg n implies LaplaceExpC M,i = LaplaceExpL (M @ ),i )
assume A1: i in Seg n ; :: thesis: LaplaceExpC M,i = LaplaceExpL (M @ ),i
reconsider I = i as Element of NAT by ORDINAL1:def 13;
set LC = LaplaceExpC M,i;
set LL = LaplaceExpL (M @ ),i;
A2: ( len (LaplaceExpC M,i) = n & len (LaplaceExpL (M @ ),i) = n ) by Def7, Def8;

now

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (LaplaceExpC M,i) . k = (LaplaceExpL (M @ ),i) . k )
assume A3: ( 1 <= k & k <= n ) ; :: thesis: (LaplaceExpC M,i) . k = (LaplaceExpL (M @ ),i) . k
k in NAT by ORDINAL1:def 13;
then ( k in Seg n & Indices M = [:(Seg n),(Seg n):] ) by A3, MATRIX_1:25;
then ( k in Seg n & dom (LaplaceExpC M,i) = Seg n & dom (LaplaceExpL (M @ ),i) = Seg n & [k,i] in Indices M ) by A1, A2, FINSEQ_1:def 3, ZFMISC_1:106;
then ( (LaplaceExpC M,i) . k = (M * k,I) * (Cofactor M,k,I) & (LaplaceExpL (M @ ),i) . k = ((M @ ) * I,k) * (Cofactor (M @ ),I,k) & Cofactor M,k,I = Cofactor (M @ ),I,k & M * k,I = (M @ ) * I,k ) by A1, Def7, Def8, Th24, MATRIX_1:def 7;
hence (LaplaceExpC M,i) . k = (LaplaceExpL (M @ ),i) . k ; :: thesis: verum

end;

hence LaplaceExpC M,i = LaplaceExpL (M @ ),i by A2, FINSEQ_1:18; :: thesis: verum