let i, j be Nat; :: thesis: for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = d
let D be non empty set ; :: thesis: for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = d
let d be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = d
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: ( [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) implies (block_diagonal ((F1 ^ F2),d)) * (i,j) = d )
set L1 = Len F1;
set W1 = Width F1;
set L2 = Len F2;
set W2 = Width F2;
set F12 = F1 ^ F2;
set L = Len (F1 ^ F2);
set W = Width (F1 ^ F2);
set B12 = block_diagonal ((F1 ^ F2),d);
A1: dom (block_diagonal ((F1 ^ F2),d)) = Seg (len (block_diagonal ((F1 ^ F2),d))) by FINSEQ_1:def 3;
A2: len (Width F1) = len F1 by CARD_1:def 7;
A3: len (block_diagonal ((F1 ^ F2),d)) = Sum (Len (F1 ^ F2)) by Def5;
A4: len F1 = len (Len F1) by CARD_1:def 7;
assume that
A5: [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) and
A6: ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) ; :: thesis: (block_diagonal ((F1 ^ F2),d)) * (i,j) = d
i in dom (block_diagonal ((F1 ^ F2),d)) by A5, ZFMISC_1:87;
then A7: 1 <= i by FINSEQ_3:25;
A8: (Width F1) ^ (Width F2) = Width (F1 ^ F2) by Th18;
A9: (Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
then A10: Sum (Len (F1 ^ F2)) = (Sum (Len F1)) + (Sum (Len F2)) by RVSUM_1:75;

per cases ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) by A6;

suppose A11: ( i <= Sum (Len F1) & j > Sum (Width F1) ) ; :: thesis: (block_diagonal ((F1 ^ F2),d)) * (i,j) = d

then A12: i in Seg (Sum (Len F1)) by A7;
then min ((Len F1),i) in dom (Len F1) by Def1;
then min ((Len F1),i) <= len (Len F1) by FINSEQ_3:25;
then A13: Sum ((Width (F1 ^ F2)) | (min ((Len F1),i))) <= Sum ((Width (F1 ^ F2)) | (len (Len F1))) by POLYNOM3:18;
A14: (Width (F1 ^ F2)) | (len (Len F1)) = Width F1 by A8, A2, A4, FINSEQ_5:23;
min ((Len (F1 ^ F2)),i) = min ((Len F1),i) by A9, A12, Th8;
then Sum ((Width (F1 ^ F2)) | (min ((Len (F1 ^ F2)),i))) < j by A11, A14, A13, XXREAL_0:2;
hence (block_diagonal ((F1 ^ F2),d)) * (i,j) = d by A5, Def5; :: thesis: verum

end;

suppose A15: ( i > Sum (Len F1) & j <= Sum (Width F1) ) ; :: thesis: (block_diagonal ((F1 ^ F2),d)) * (i,j) = d

A16: i in Seg (Sum (Len (F1 ^ F2))) by A1, A3, A5, ZFMISC_1:87;
not i in Seg (Sum (Len F1)) by A15, FINSEQ_1:1;
then A17: i in (Seg ((Sum (Len F1)) + (Sum (Len F2)))) \ (Seg (Sum (Len F1))) by A10, A16, XBOOLE_0:def 5;
then A18: i -' (Sum (Len F1)) = i - (Sum (Len F1)) by Th9;
then A19: i = (i -' (Sum (Len F1))) + (Sum (Len F1)) ;
i -' (Sum (Len F1)) <> 0 by A15, A18;
then i -' (Sum (Len F1)) in Seg (Sum (Len F2)) by A10, A16, A19, FINSEQ_1:61;
then min ((Len F2),(i -' (Sum (Len F1)))) in dom (Len F2) by Def1;
then A20: min ((Len F2),(i -' (Sum (Len F1)))) >= 1 by FINSEQ_3:25;
min ((Len (F1 ^ F2)),i) = (min ((Len F2),(i -' (Sum (Len F1))))) + (len (Len F1)) by A9, A17, Th9;
then (min ((Len (F1 ^ F2)),i)) -' 1 = ((min ((Len F2),(i -' (Sum (Len F1))))) -' 1) + (len (Len F1)) by A20, NAT_D:38;
then (min ((Len (F1 ^ F2)),i)) -' 1 >= (len (Len F1)) + 0 by XREAL_1:7;
then A21: Sum ((Width (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1)) >= Sum (((Width F1) ^ (Width F2)) | (len (Width F1))) by A8, A2, A4, POLYNOM3:18;
((Width F1) ^ (Width F2)) | (len (Width F1)) = Width F1 by FINSEQ_5:23;
then Sum ((Width (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1)) >= j by A15, A21, XXREAL_0:2;
hence (block_diagonal ((F1 ^ F2),d)) * (i,j) = d by A5, Def5; :: thesis: verum

end;

end;