let D be non empty set ; 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; 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; 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 ;
TARSKI:def 3 ( 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))
;
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;
verum
end;
hence
Indices (block_diagonal (F1,d1)) is Subset of (Indices (block_diagonal ((F1 ^ F2),d2)))
; verum