let K be Field; :: thesis: for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 holds
(block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))
let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: ( Width R1 = Len R2 implies (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K)) )
defpred S₁[ Nat] means for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 & len R1 = $1 holds
(block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K));
assume A1: Width R1 = Len R2 ; :: thesis: (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: ( Width R1 = Len R2 & len R1 = n + 1 implies (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K)) )
assume that
A4: Width R1 = Len R2 and
A5: len R1 = n + 1 ; :: thesis: (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))
A6: n + 1 in Seg (n + 1) by FINSEQ_1:4;
set R1n = R1 | n;
A7: len (R1 | n) = n by A5, FINSEQ_1:59, NAT_1:11;
set R2n = R2 | n;
A8: len R1 = len (Len R2) by A4, CARD_1:def 7
.= len R2 by CARD_1:def 7 ;
then A9: len (R2 | n) = n by A5, FINSEQ_1:59, NAT_1:11;
set b2n = block_diagonal ((R2 | n),(0. K));
set b1n = block_diagonal ((R1 | n),(0. K));
A10: Width (R1 | n) = (Width R1) | n by Th21
.= Len (R2 | n) by A4, Th17 ;
A11: dom (Width R1) = Seg (n + 1) by A5, FINSEQ_2:124;
then A12: width (R1 . (n + 1)) = (Len R2) . (n + 1) by A4, A6, Def4
.= len (R2 . (n + 1)) by A4, A6, A11, Def3 ;
A13: R1 = (R1 | n) ^ <*(R1 . (n + 1))*> by A5, FINSEQ_3:55;
A14: width (block_diagonal ((R1 | n),(0. K))) = Sum (Width (R1 | n)) by Def5
.= len (block_diagonal ((R2 | n),(0. K))) by A10, Def5 ;
A15: R2 = (R2 | n) ^ <*(R2 . (n + 1))*> by A5, A8, FINSEQ_3:55;
hence (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = (block_diagonal (<*(block_diagonal ((R1 | n),(0. K))),(R1 . (n + 1))*>,(0. K))) * (block_diagonal (((R2 | n) ^ <*(R2 . (n + 1))*>),(0. K))) by A13, Th35
.= (block_diagonal (<*(block_diagonal ((R1 | n),(0. K))),(R1 . (n + 1))*>,(0. K))) * (block_diagonal (<*(block_diagonal ((R2 | n),(0. K))),(R2 . (n + 1))*>,(0. K))) by Th35
.= block_diagonal ((<*(block_diagonal ((R1 | n),(0. K))),(R1 . (n + 1))*> (#) <*(block_diagonal ((R2 | n),(0. K))),(R2 . (n + 1))*>),(0. K)) by A14, A12, Th78
.= block_diagonal (<*((block_diagonal ((R1 | n),(0. K))) * (block_diagonal ((R2 | n),(0. K)))),((R1 . (n + 1)) * (R2 . (n + 1)))*>,(0. K)) by Th77
.= block_diagonal (<*(block_diagonal (((R1 | n) (#) (R2 | n)),(0. K))),((R1 . (n + 1)) * (R2 . (n + 1)))*>,(0. K)) by A3, A7, A10
.= block_diagonal ((((R1 | n) (#) (R2 | n)) ^ <*((R1 . (n + 1)) * (R2 . (n + 1)))*>),(0. K)) by Th35
.= block_diagonal ((((R1 | n) (#) (R2 | n)) ^ (<*(R1 . (n + 1))*> (#) <*(R2 . (n + 1))*>)),(0. K)) by Th76
.= block_diagonal ((R1 (#) R2),(0. K)) by A7, A9, A13, A15, Th74 ;
:: thesis: verum

end;

A16: S₁[ 0 ]

proof

let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: ( Width R1 = Len R2 & len R1 = 0 implies (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K)) )
assume that
A17: Width R1 = Len R2 and
A18: len R1 = 0 ; :: thesis: (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))
A19: Sum (Width R1) = 0 by A18, RVSUM_1:72;
set b2 = block_diagonal (R2,(0. K));
Len R2 = {} by A17, A18;
then A20: len (block_diagonal (R2,(0. K))) = 0 by Def5, RVSUM_1:72;
set b1 = block_diagonal (R1,(0. K));
A21: Sum (Width R1) = width (block_diagonal (R1,(0. K))) by Def5;
set b12 = block_diagonal ((R1 (#) R2),(0. K));
A22: Len R1 = {} by A18;
Len R1 = Len (R1 (#) R2) by A17, Th73;
then len (block_diagonal ((R1 (#) R2),(0. K))) = 0 by A22, Def5, RVSUM_1:72;
then A23: block_diagonal ((R1 (#) R2),(0. K)) = {} ;
len (block_diagonal (R1,(0. K))) = 0 by A22, Def5, RVSUM_1:72;
then len ((block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K)))) = 0 by A20, A21, A19, MATRIX_3:def 4;
hence (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K)) by A23; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A2);
hence (block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K)) by A1; :: thesis: verum