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 ;
then A7: (LaplaceExpC (M,i)) . k = (M * (k,I)) * (Cofactor (M,k,I)) by ;
Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A8: [k,i] in Indices M by ;
dom (LaplaceExpL ((M @),i)) = Seg n by ;
then A9: (LaplaceExpL ((M @),i)) . k = ((M @) * (I,k)) * (Cofactor ((M @),I,k)) by ;
Cofactor (M,k,I) = Cofactor ((M @),I,k) by A1, A6, Th24;
hence (LaplaceExpC (M,i)) . k = (LaplaceExpL ((M @),i)) . k by ; :: thesis: verum
end;
hence LaplaceExpC (M,i) = LaplaceExpL ((M @),i) by A3, A2; :: thesis: verum