let K be Field; :: thesis: for R being FinSequence_of_Square-Matrix of K holds Det (block_diagonal R,(0. K)) = Product (Det R)
let R be FinSequence_of_Square-Matrix of K; :: thesis: Det (block_diagonal R,(0. K)) = Product (Det R)
defpred S₁[ Nat] means for R being FinSequence_of_Square-Matrix of K st len R = $1 holds
Det (block_diagonal R,(0. K)) = Product (Det R);
A1: S₁[ 0 ]

proof

let R be FinSequence_of_Square-Matrix of K; :: thesis: ( len R = 0 implies Det (block_diagonal R,(0. K)) = Product (Det R) )
assume A2: len R = 0 ; :: thesis: Det (block_diagonal R,(0. K)) = Product (Det R)
len (Len R) = 0 by A2, FINSEQ_1:def 18;
then Len R = {} ;
then Sum (Len R) = 0 by RVSUM_1:102;
hence Det (block_diagonal R,(0. K)) = 1_ K by MATRIXR2:41
.= Product (Det R) by A2, FVSUM_1:105 ;
:: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let R be FinSequence_of_Square-Matrix of K; :: thesis: ( len R = n + 1 implies Det (block_diagonal R,(0. K)) = Product (Det R) )
assume A5: len R = n + 1 ; :: thesis: Det (block_diagonal R,(0. K)) = Product (Det R)
set Rn = R | n;
set bR = block_diagonal (R | n),(0. K);
set R1 = R . (n + 1);
A6: R = (R | n) ^ <*(R . (n + 1))*> by A5, FINSEQ_3:61;
A7: Sum (Len <*(block_diagonal (R | n),(0. K)),(R . (n + 1))*>) = (len (block_diagonal (R | n),(0. K))) + (len (R . (n + 1))) by Th16
.= (Sum (Len (R | n))) + (len (R . (n + 1))) by Def5
.= Sum ((Len (R | n)) ^ <*(len (R . (n + 1)))*>) by RVSUM_1:104
.= Sum ((Len (R | n)) ^ (Len <*(R . (n + 1))*>)) by Th15
.= Sum (Len R) by A6, Th14 ;
A8: len (R | n) = n by A5, FINSEQ_1:80, NAT_1:11;
block_diagonal R,(0. K) = block_diagonal <*(block_diagonal (R | n),(0. K)),(R . (n + 1))*>,(0. K) by A6, Th35;
hence Det (block_diagonal R,(0. K)) = (Det (block_diagonal (R | n),(0. K))) * (Det (R . (n + 1))) by A7, Th52
.= (Product (Det (R | n))) * (Det (R . (n + 1))) by A4, A8
.= Product ((Det (R | n)) ^ <*(Det (R . (n + 1)))*>) by GROUP_4:9
.= Product ((Det (R | n)) ^ (Det <*(R . (n + 1))*>)) by Th49
.= Product (Det R) by A6, Th50 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence Det (block_diagonal R,(0. K)) = Product (Det R) ; :: thesis: verum