let D be non empty set ; :: thesis: for d1, d2 being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds Indices (block_diagonal F1,d1) is Subset of (Indices (block_diagonal (F1 ^ F2),d2))
let d1, d2 be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D holds Indices (block_diagonal F1,d1) is Subset of (Indices (block_diagonal (F1 ^ F2),d2))
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: Indices (block_diagonal F1,d1) is Subset of (Indices (block_diagonal (F1 ^ F2),d2))
set B1 = block_diagonal F1,d1;
set B2 = block_diagonal (F1 ^ F2),d2;
Indices (block_diagonal F1,d1) c= Indices (block_diagonal (F1 ^ F2),d2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Indices (block_diagonal F1,d1) or x in Indices (block_diagonal (F1 ^ F2),d2) )
assume A1: x in Indices (block_diagonal F1,d1) ; :: thesis: x in Indices (block_diagonal (F1 ^ F2),d2)
consider i, j being set such that
A2: ( i in dom (block_diagonal F1,d1) & j in Seg (width (block_diagonal F1,d1)) & x = [i,j] ) by A1, ZFMISC_1:def 2;
A3: ( dom (block_diagonal F1,d1) = Seg (len (block_diagonal F1,d1)) & dom (block_diagonal (F1 ^ F2),d2) = Seg (len (block_diagonal (F1 ^ F2),d2)) ) by FINSEQ_1:def 3;
A4: ( len (block_diagonal (F1 ^ F2),d2) = Sum (Len (F1 ^ F2)) & len (block_diagonal F1,d1) = Sum (Len F1) & width (block_diagonal (F1 ^ F2),d2) = Sum (Width (F1 ^ F2)) & width (block_diagonal F1,d1) = Sum (Width F1) ) by Def5;
( (Len F1) ^ (Len F2) = Len (F1 ^ F2) & (Width F1) ^ (Width F2) = Width (F1 ^ F2) ) by Th14, Th18;
then ( (Sum (Len F1)) + (Sum (Len F2)) = Sum (Len (F1 ^ F2)) & (Sum (Width F1)) + (Sum (Width F2)) = Sum (Width (F1 ^ F2)) ) by RVSUM_1:105;
then ( 0 + (Sum (Len F1)) <= Sum (Len (F1 ^ F2)) & 0 + (Sum (Width F1)) <= Sum (Width (F1 ^ F2)) ) by XREAL_1:8;
then ( Seg (Sum (Len F1)) c= Seg (Sum (Len (F1 ^ F2))) & Seg (Sum (Width F1)) c= Seg (Sum (Width (F1 ^ F2))) ) by FINSEQ_1:7;
hence x in Indices (block_diagonal (F1 ^ F2),d2) by A2, A3, A4, ZFMISC_1:106; :: thesis: verum

end;

hence Indices (block_diagonal F1,d1) is Subset of (Indices (block_diagonal (F1 ^ F2),d2)) ; :: thesis: verum