let i, j be Nat; :: thesis: for D being non empty set
for d1, d2 being Element of D
for F2, F1 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 F2, F1 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 F2, F1 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 F2, F1 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 F2,d1) = Seg (len (block_diagonal F2,d1)) & 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)) & len (block_diagonal F2,d1) = Sum (Len F2) & width (block_diagonal (F1 ^ F2),d2) = Sum (Width (F1 ^ F2)) & width (block_diagonal F2,d1) = Sum (Width F2) ) by Def5;
( (Len F1) ^ (Len F2) = Len (F1 ^ F2) & (Width F1) ^ (Width F2) = Width (F1 ^ F2) ) by Th14, Th18;
then A3: ( (Sum (Len F1)) + (Sum (Len F2)) = Sum (Len (F1 ^ F2)) & (Sum (Width F1)) + (Sum (Width F2)) = Sum (Width (F1 ^ F2)) ) by RVSUM_1:105;

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 [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 ( i in Seg (len (block_diagonal F2,d1)) & j in Seg (width (block_diagonal F2,d1)) ) by A1, ZFMISC_1:106;
then ( i > 0 & j > 0 & i + (Sum (Len F1)) in Seg (len (block_diagonal (F1 ^ F2),d2)) & j + (Sum (Width F1)) in Seg (width (block_diagonal (F1 ^ F2),d2)) ) by A2, A3, FINSEQ_1:3, FINSEQ_1:81;
hence ( i > 0 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal (F1 ^ F2),d2) ) by A1, ZFMISC_1:106; :: thesis: verum

end;

assume that
A4: ( i > 0 & j > 0 ) and
A5: [(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)) & j + (Sum (Width F1)) in Seg (width (block_diagonal (F1 ^ F2),d2)) ) by A1, A5, ZFMISC_1:106;
then ( i in Seg (len (block_diagonal F2,d1)) & j in Seg (width (block_diagonal F2,d1)) & dom (block_diagonal F2,d1) = Seg (len (block_diagonal F2,d1)) ) by A2, A3, A4, FINSEQ_1:82, FINSEQ_1:def 3;
hence [i,j] in Indices (block_diagonal F2,d1) by ZFMISC_1:106; :: thesis: verum