let K be Field; :: thesis: for a1, a2 being Element of K
for R1, R2 being FinSequence_of_Square-Matrix of K st Len R1 = Len R2 & Width R1 = Width R2 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
let a1, a2 be Element of K; :: thesis: for R1, R2 being FinSequence_of_Square-Matrix of K st Len R1 = Len R2 & Width R1 = Width R2 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: ( Len R1 = Len R2 & Width R1 = Width R2 implies (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2)) )
defpred S₁[ Nat] means for R1, R2 being FinSequence_of_Square-Matrix of K
for a1, a2 being Element of K st Len R1 = Len R2 & Width R1 = Width R2 & len R1 = $1 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2));
assume that
A1: Len R1 = Len R2 and
A2: Width R1 = Width R2 ; :: thesis: (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
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 R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: for a1, a2 being Element of K st Len R1 = Len R2 & Width R1 = Width R2 & len R1 = n + 1 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
let a1, a2 be Element of K; :: thesis: ( Len R1 = Len R2 & Width R1 = Width R2 & len R1 = n + 1 implies (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2)) )
assume that
A5: Len R1 = Len R2 and
A6: Width R1 = Width R2 and
A7: len R1 = n + 1 ; :: thesis: (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
A8: n + 1 in Seg (n + 1) by FINSEQ_1:4;
set R2n = R2 | n;
A9: R1 = (R1 | n) ^ <*(R1 . (n + 1))*> by A7, FINSEQ_3:55;
set R1n = R1 | n;
set b2n = block_diagonal ((R2 | n),a2);
set b1n = block_diagonal ((R1 | n),a1);
A10: len (R1 | n) = n by A7, FINSEQ_1:59, NAT_1:11;
A11: dom (Len R1) = Seg (n + 1) by A7, FINSEQ_2:124;
then A12: len (R1 . (n + 1)) = (Len R1) . (n + 1) by A8, Def3
.= len (R2 . (n + 1)) by A5, A8, A11, Def3 ;
A13: len R1 = len (Len R2) by A5, CARD_1:def 7
.= len R2 by CARD_1:def 7 ;
then A14: len (R2 | n) = n by A7, FINSEQ_1:59, NAT_1:11;
A15: dom (Width R1) = Seg (n + 1) by A7, FINSEQ_2:124;
then A16: width (R1 . (n + 1)) = (Width R1) . (n + 1) by A8, Def4
.= width (R2 . (n + 1)) by A6, A8, A15, Def4 ;
A17: Len (R1 | n) = (Len R1) | n by Th17
.= Len (R2 | n) by A5, Th17 ;
then A18: len (block_diagonal ((R1 | n),a1)) = Sum (Len (R2 | n)) by Def5
.= len (block_diagonal ((R2 | n),a2)) by Def5 ;
A19: Width (R1 | n) = (Width R1) | n by Th21
.= Width (R2 | n) by A6, Th21 ;
then A20: width (block_diagonal ((R1 | n),a1)) = Sum (Width (R2 | n)) by Def5
.= width (block_diagonal ((R2 | n),a2)) by Def5 ;
A21: R2 = (R2 | n) ^ <*(R2 . (n + 1))*> by A7, A13, FINSEQ_3:55;
hence (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = (block_diagonal (<*(block_diagonal ((R1 | n),a1)),(R1 . (n + 1))*>,a1)) + (block_diagonal (((R2 | n) ^ <*(R2 . (n + 1))*>),a2)) by A9, Th35
.= (block_diagonal (<*(block_diagonal ((R1 | n),a1)),(R1 . (n + 1))*>,a1)) + (block_diagonal (<*(block_diagonal ((R2 | n),a2)),(R2 . (n + 1))*>,a2)) by Th35
.= block_diagonal ((<*(block_diagonal ((R1 | n),a1)),(R1 . (n + 1))*> (+) <*(block_diagonal ((R2 | n),a2)),(R2 . (n + 1))*>),(a1 + a2)) by A18, A20, A12, A16, Th71
.= block_diagonal (<*((block_diagonal ((R1 | n),a1)) + (block_diagonal ((R2 | n),a2))),((R1 . (n + 1)) + (R2 . (n + 1)))*>,(a1 + a2)) by Th70
.= block_diagonal (<*(block_diagonal (((R1 | n) (+) (R2 | n)),(a1 + a2))),((R1 . (n + 1)) + (R2 . (n + 1)))*>,(a1 + a2)) by A4, A10, A17, A19
.= block_diagonal ((((R1 | n) (+) (R2 | n)) ^ <*((R1 . (n + 1)) + (R2 . (n + 1)))*>),(a1 + a2)) by Th35
.= block_diagonal ((((R1 | n) (+) (R2 | n)) ^ (<*(R1 . (n + 1))*> (+) <*(R2 . (n + 1))*>)),(a1 + a2)) by Th69
.= block_diagonal ((R1 (+) R2),(a1 + a2)) by A10, A14, A9, A21, Th67 ;
:: thesis: verum

end;

A22: S₁[ 0 ]

proof

let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: for a1, a2 being Element of K st Len R1 = Len R2 & Width R1 = Width R2 & len R1 = 0 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
let a1, a2 be Element of K; :: thesis: ( Len R1 = Len R2 & Width R1 = Width R2 & len R1 = 0 implies (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2)) )
assume that
Len R1 = Len R2 and
Width R1 = Width R2 and
A23: len R1 = 0 ; :: thesis: (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
set b12 = block_diagonal ((R1 (+) R2),(a1 + a2));
set b2 = block_diagonal (R2,a2);
set b1 = block_diagonal (R1,a1);
A24: Len R1 = {} by A23;
Len R1 = Len (R1 (+) R2) by Th66;
then len (block_diagonal ((R1 (+) R2),(a1 + a2))) = 0 by A24, Def5, RVSUM_1:72;
then A25: block_diagonal ((R1 (+) R2),(a1 + a2)) = {} ;
len (block_diagonal (R1,a1)) = 0 by A24, Def5, RVSUM_1:72;
then len ((block_diagonal (R1,a1)) + (block_diagonal (R2,a2))) = 0 by MATRIX_3:def 3;
hence (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2)) by A25; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A22, A3);
hence (block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2)) by A1, A2; :: thesis: verum