let i, j be Nat; :: thesis: for D being non empty set
for d1, d2 being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds
( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )
let D be non empty set ; :: thesis: for d1, d2 being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds
( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )
let d1, d2 be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D holds
( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: ( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )
set B2 = block_diagonal (F2,d1);
set B12 = block_diagonal ((F1 ^ F2),d2);
A1: dom (block_diagonal ((F1 ^ F2),d2)) = Seg (len (block_diagonal ((F1 ^ F2),d2))) by FINSEQ_1:def 3;
A2: len (block_diagonal ((F1 ^ F2),d2)) = Sum (Len (F1 ^ F2)) by Def5;
(Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
then A3: (Sum (Len F1)) + (Sum (Len F2)) = Sum (Len (F1 ^ F2)) by RVSUM_1:75;
A4: len (block_diagonal (F2,d1)) = Sum (Len F2) by Def5;
(Width F1) ^ (Width F2) = Width (F1 ^ F2) by Th18;
then A5: (Sum (Width F1)) + (Sum (Width F2)) = Sum (Width (F1 ^ F2)) by RVSUM_1:75;
A6: width (block_diagonal ((F1 ^ F2),d2)) = Sum (Width (F1 ^ F2)) by Def5;
A7: width (block_diagonal (F2,d1)) = Sum (Width F2) by Def5;
A8: dom (block_diagonal (F2,d1)) = Seg (len (block_diagonal (F2,d1))) by FINSEQ_1:def 3;

hereby :: thesis: ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) implies [i,j] in Indices (block_diagonal (F2,d1)) )

assume A9: [i,j] in Indices (block_diagonal (F2,d1)) ; :: thesis: ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) )
then A10: j in Seg (width (block_diagonal (F2,d1))) by ZFMISC_1:87;
then A11: j + (Sum (Width F1)) in Seg (width (block_diagonal ((F1 ^ F2),d2))) by A6, A7, A5, FINSEQ_1:60;
A12: i in Seg (len (block_diagonal (F2,d1))) by A8, A9, ZFMISC_1:87;
then i + (Sum (Len F1)) in Seg (len (block_diagonal ((F1 ^ F2),d2))) by A2, A4, A3, FINSEQ_1:60;
hence ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) by A1, A12, A10, A11, ZFMISC_1:87; :: thesis: verum

end;

assume that
A13: i > 0 and
A14: j > 0 and
A15: [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ; :: thesis: [i,j] in Indices (block_diagonal (F2,d1))
i + (Sum (Len F1)) in Seg (len (block_diagonal ((F1 ^ F2),d2))) by A1, A15, ZFMISC_1:87;
then A16: i in Seg (len (block_diagonal (F2,d1))) by A2, A4, A3, A13, FINSEQ_1:61;
j + (Sum (Width F1)) in Seg (width (block_diagonal ((F1 ^ F2),d2))) by A15, ZFMISC_1:87;
then A17: j in Seg (width (block_diagonal (F2,d1))) by A6, A7, A5, A14, FINSEQ_1:61;
dom (block_diagonal (F2,d1)) = Seg (len (block_diagonal (F2,d1))) by FINSEQ_1:def 3;
hence [i,j] in Indices (block_diagonal (F2,d1)) by A16, A17, ZFMISC_1:87; :: thesis: verum