let K be Field; :: thesis: for a being Element of K holds Det <*<*a*>*> = a
let a be Element of K; :: thesis: Det <*<*a*>*> = a
set M = <*<*a*>*>;
A1: (Path_product <*<*a*>*>) . (idseq 1) = a

proof

reconsider p = idseq 1 as Element of Permutations 1 by MATRIX_1:def 12;
A2: - (a,p) = a

proof

reconsider q = id (Seg 1) as Element of Permutations 1 by MATRIX_1:def 12;
len (Permutations 1) = 1 by MATRIX_1:9;
then q is even by MATRIX_1:16;
hence - (a,p) = a by MATRIX_1:def 16; :: thesis: verum

end;

A3: len (Path_matrix (p,<*<*a*>*>)) = 1 by Def7;
then A4: dom (Path_matrix (p,<*<*a*>*>)) = Seg 1 by FINSEQ_1:def 3;
then A5: 1 in dom (Path_matrix (p,<*<*a*>*>)) by FINSEQ_1:2, TARSKI:def 1;
then 1 = p . 1 by A4, FUNCT_1:18;
then (Path_matrix (p,<*<*a*>*>)) . 1 = <*<*a*>*> * (1,1) by A5, Def7;
then (Path_matrix (p,<*<*a*>*>)) . 1 = a by MATRIX_0:49;
then A6: Path_matrix (p,<*<*a*>*>) = <*a*> by A3, FINSEQ_1:40;
( (Path_product <*<*a*>*>) . p = - (( the multF of K $$ (Path_matrix (p,<*<*a*>*>))),p) & <*a*> = 1 |-> a ) by Def8, FINSEQ_2:59;
hence (Path_product <*<*a*>*>) . (idseq 1) = a by A6, A2, FINSOP_1:16; :: thesis: verum

end;

( FinOmega (Permutations 1) = {(idseq 1)} & idseq 1 in Permutations 1 ) by MATRIX_1:10, FINSUB_1:def 6, TARSKI:def 1;
hence Det <*<*a*>*> = a by A1, SETWISEO:17; :: thesis: verum