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: - 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;

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:4, TARSKI:def 1;
then 1 = p . 1 by A4, FUNCT_1:35;
then (Path_matrix p,<*<*a*>*>) . 1 = <*<*a*>*> * 1,1 by A5, Def7;
then (Path_matrix p,<*<*a*>*>) . 1 = a by MATRIX_2:5;
then A6: Path_matrix p,<*<*a*>*> = <*a*> by A3, FINSEQ_1:57;
( (Path_product <*<*a*>*>) . p = - (the multF of K $$ (Path_matrix p,<*<*a*>*>)),p & <*a*> = 1 |-> a ) by Def8, FINSEQ_2:73;
hence (Path_product <*<*a*>*>) . (idseq 1) = a by A6, A2, FINSOP_1:17; :: thesis: verum

end;

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