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: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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 A3: len R = n + 1 ; :: thesis: Det (block_diagonal (R,(0. K))) = Product (Det R)
set Rn = R | n;
A4: len (R | n) = n by A3, FINSEQ_1:59, NAT_1:11;
set R1 = R . (n + 1);
set bR = block_diagonal ((R | n),(0. K));
A5: R = (R | n) ^ <*(R . (n + 1))*> by A3, FINSEQ_3:55;
then A6: block_diagonal (R,(0. K)) = block_diagonal (<*(block_diagonal ((R | n),(0. K))),(R . (n + 1))*>,(0. K)) by Th35;
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:74
.= Sum ((Len (R | n)) ^ (Len <*(R . (n + 1))*>)) by Th15
.= Sum (Len R) by A5, Th14 ;
hence Det (block_diagonal (R,(0. K))) = (Det (block_diagonal ((R | n),(0. K)))) * (Det (R . (n + 1))) by A6, Th52
.= (Product (Det (R | n))) * (Det (R . (n + 1))) by A2, A4
.= Product ((Det (R | n)) ^ <*(Det (R . (n + 1)))*>) by GROUP_4:6
.= Product ((Det (R | n)) ^ (Det <*(R . (n + 1))*>)) by Th49
.= Product (Det R) by A5, Th50 ;
:: thesis: verum

end;

A7: 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 A8: len R = 0 ; :: thesis: Det (block_diagonal (R,(0. K))) = Product (Det R)
Len R = {} by A8;
hence Det (block_diagonal (R,(0. K))) = 1_ K by MATRIXR2:41, RVSUM_1:72
.= Product (Det R) by A8, FVSUM_1:80 ;
:: thesis: verum

end;

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