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:6;
set R2n = R2 | n;
A9: R1 = (R1 | n) ^ <*(R1 . (n + 1))*> by A7, FINSEQ_3:61;
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:80, NAT_1:11;
A11: dom (Len R1) = Seg (n + 1) by A7, FINSEQ_2:144;
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, FINSEQ_1:def 18
.= len R2 by FINSEQ_1:def 18 ;
then A14: len (R2 | n) = n by A7, FINSEQ_1:80, NAT_1:11;
A15: dom (Width R1) = Seg (n + 1) by A7, FINSEQ_2:144;
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:61;
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:102;
then A25: block_diagonal (R1 (+) R2),(a1 + a2) = {} ;
len (block_diagonal R1,a1) = 0 by A24, Def5, RVSUM_1:102;
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