let K be Field; :: thesis: for A being Matrix of 0 ,K holds Det A = 1. K
reconsider kk = idseq 0 as Element of Permutations 0 by Th40, TARSKI:def 1;
let A be Matrix of 0 ,K; :: thesis: Det A = 1. K
A1: (Path_product A) . (idseq 0 ) = 1. K

proof

reconsider p = idseq 0 as Element of Permutations 0 by Lm4, MATRIX_2:def 11;
A2: - (1_ K),p = 1_ K

proof

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

end;

1_ K is_a_unity_wrt the multF of K by GROUP_1:32;
then ( len (Path_matrix p,A) = 0 & the multF of K is having_a_unity ) by MATRIX_3:def 7, SETWISEO:def 2;
then the multF of K $$ (Path_matrix p,A) = the_unity_wrt the multF of K by FINSOP_1:def 1
.= 1_ K by GROUP_1:33 ;
hence (Path_product A) . (idseq 0 ) = 1. K by A2, MATRIX_3:def 8; :: thesis: verum

end;

A3: FinOmega (Permutations 0 ) = Permutations 0 by Th40, MATRIX_2:def 17
.= {.kk.} by Th40 ;
Det A = the addF of K $$ (FinOmega (Permutations 0 )),(Path_product A) by MATRIX_3:def 9
.= 1. K by A1, A3, SETWISEO:26 ;
hence Det A = 1. K ; :: thesis: verum