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
set LL = LaplaceExpL (M @ ),i;
set LC = LaplaceExpC M,i;
reconsider I = i as Element of NAT by ORDINAL1:def 13;
A2: len (LaplaceExpL (M @ ),i) = n by Def7;
A3: len (LaplaceExpC M,i) = n by Def8;

now

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

end;

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