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_2:def 11;
A2: len (Path_matrix p,<*<*a*>*>) = 1 by Def7;
then A3: dom (Path_matrix p,<*<*a*>*>) = Seg 1 by FINSEQ_1:def 3;
then A4: 1 in dom (Path_matrix p,<*<*a*>*>) by FINSEQ_1:4, TARSKI:def 1;
then 1 = p . 1 by A3, FUNCT_1:35;
then (Path_matrix p,<*<*a*>*>) . 1 = <*<*a*>*> * 1,1 by A4, Def7;
then (Path_matrix p,<*<*a*>*>) . 1 = a by MATRIX_2:5;
then A5: Path_matrix p,<*<*a*>*> = <*a*> by A2, FINSEQ_1:57;
A6: (Path_product <*<*a*>*>) . p = - (the multF of K $$ (Path_matrix p,<*<*a*>*>)),p by Def8;
A7: <*a*> = 1 |-> a by FINSEQ_2:73;
- a,p = a

proof

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

end;

hence (Path_product <*<*a*>*>) . (idseq 1) = a by A5, A6, A7, FINSOP_1:17; :: thesis: verum

end;

A8: FinOmega (Permutations 1) = {(idseq 1)} by MATRIX_2:21, MATRIX_2:def 17;
idseq 1 in Permutations 1 by MATRIX_2:21, TARSKI:def 1;
hence Det <*<*a*>*> = a by A1, A8, SETWISEO:26; :: thesis: verum