let K be Ring; :: 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_1:def 12;
A2: - ((1_ K),p) = 1_ K
proof
reconsider q = id (Seg 0) as Element of Permutations 0 by Lm4, MATRIX_1:def 12;
len (Permutations 0) = 0 by MATRIX_1:9;
then q is even by MATRIX_1:16;
hence - ((1_ K),p) = 1_ K by MATRIX_1:def 16; :: thesis: verum
end;
1_ K is_a_unity_wrt the multF of K by GROUP_1:21;
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:22 ;
hence (Path_product A) . (idseq 0) = 1. K by A2, MATRIX_3:def 8; :: thesis: verum
end;
Permutations 0 in Fin (Permutations 0) by FINSUB_1:def 5;
then A3: In ((Permutations 0),(Fin (Permutations 0))) = Permutations 0 by SUBSET_1:def 8
.= {.kk.} by Th40 ;
Det A = the addF of K $$ ((In ((Permutations 0),(Fin (Permutations 0)))),(Path_product A)) by MATRIX_3:def 9
.= 1. K by A1, A3, SETWISEO:17 ;
hence Det A = 1. K ; :: thesis: verum