let i, j be Nat; 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 ; 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; 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; ( [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:105;
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:105;
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:106;
then A11:
j + (Sum (Width F1)) in Seg (width (block_diagonal (F1 ^ F2),d2))
by A6, A7, A5, FINSEQ_1:81;
A12:
i in Seg (len (block_diagonal F2,d1))
by A8, A9, ZFMISC_1:106;
then
i + (Sum (Len F1)) in Seg (len (block_diagonal (F1 ^ F2),d2))
by A2, A4, A3, 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, A12, A10, A11, FINSEQ_1:3, ZFMISC_1:106;
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:106;
then A16:
i in Seg (len (block_diagonal F2,d1))
by A2, A4, A3, A13, FINSEQ_1:82;
j + (Sum (Width F1)) in Seg (width (block_diagonal (F1 ^ F2),d2))
by A15, ZFMISC_1:106;
then A17:
j in Seg (width (block_diagonal F2,d1))
by A6, A7, A5, A14, FINSEQ_1:82;
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:106; verum