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

(Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
then (Sum (Len F1)) + (Sum (Len F2)) = Sum (Len (F1 ^ F2)) by RVSUM_1:75;
then 0 + (Sum (Len F1)) <= Sum (Len (F1 ^ F2)) by XREAL_1:6;
then A1: Seg (Sum (Len F1)) c= Seg (Sum (Len (F1 ^ F2))) by FINSEQ_1:5;
A2: dom (block_diagonal ((F1 ^ F2),d2)) = Seg (len (block_diagonal ((F1 ^ F2),d2))) by FINSEQ_1:def 3;
(Width F1) ^ (Width F2) = Width (F1 ^ F2) by Th18;
then (Sum (Width F1)) + (Sum (Width F2)) = Sum (Width (F1 ^ F2)) by RVSUM_1:75;
then 0 + (Sum (Width F1)) <= Sum (Width (F1 ^ F2)) by XREAL_1:6;
then A3: Seg (Sum (Width F1)) c= Seg (Sum (Width (F1 ^ F2))) by FINSEQ_1:5;
A4: len (block_diagonal (F1,d1)) = Sum (Len F1) by Def5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Indices (block_diagonal (F1,d1)) or x in Indices (block_diagonal ((F1 ^ F2),d2)) )
assume x in Indices (block_diagonal (F1,d1)) ; :: thesis: x in Indices (block_diagonal ((F1 ^ F2),d2))
then A5: ex i, j being object st
( i in dom (block_diagonal (F1,d1)) & j in Seg (width (block_diagonal (F1,d1))) & x = [i,j] ) by ZFMISC_1:def 2;
A6: dom (block_diagonal (F1,d1)) = Seg (len (block_diagonal (F1,d1))) by FINSEQ_1:def 3;
A7: width (block_diagonal (F1,d1)) = Sum (Width F1) by Def5;
A8: width (block_diagonal ((F1 ^ F2),d2)) = Sum (Width (F1 ^ F2)) by Def5;
len (block_diagonal ((F1 ^ F2),d2)) = Sum (Len (F1 ^ F2)) by Def5;
hence x in Indices (block_diagonal ((F1 ^ F2),d2)) by A5, A6, A2, A4, A8, A7, A1, A3, ZFMISC_1:87; :: thesis: verum

end;

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