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 12;
A2: len (LaplaceExpL ((M @),i)) = n by Def7;
A3: len (LaplaceExpC (M,i)) = n by Def8;

now :: thesis: for k being Nat st 1 <= k & k <= n holds
(LaplaceExpC (M,i)) . k = (LaplaceExpL ((M @),i)) . k

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
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_0:24;
then A8: [k,i] in Indices M by A1, A6, ZFMISC_1:87;
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_0:def 6; :: thesis: verum

end;

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