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;

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

hence
LaplaceExpC (M,i) = LaplaceExpL ((M @),i)
by A3, A2; :: thesis: verum(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;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