let n be Nat; :: thesis: for K being Field
for N being Matrix of n,K holds Det <*N*> = <*(Det N)*>
let K be Field; :: thesis: for N being Matrix of n,K holds Det <*N*> = <*(Det N)*>
let N be Matrix of n,K; :: thesis: Det <*N*> = <*(Det N)*>
set F = <*N*>;
A1: len <*N*> = 1 by FINSEQ_1:40;
A2: n = len N by MATRIX_0:def 2;
A3: <*N*> . 1 = N by FINSEQ_1:40;
A4: len <*N*> = len (Det <*N*>) by CARD_1:def 7;
A5: dom (Det <*N*>) = Seg (len <*N*>) by FINSEQ_2:124;
1 in Seg 1 ;
then (Det <*N*>) . 1 = Det (<*N*> . 1) by A1, A5, Def7;
hence Det <*N*> = <*(Det N)*> by A1, A4, A3, A2, FINSEQ_1:40; :: thesis: verum