let i, j be Nat; 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 ; 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; 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; ( [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 ( 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))
;
( 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;
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))
; [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; verum