let i, j be Nat; for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1 ^ F2),d) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal (F1 ^ F2),d) * i,j = d
let D be non empty set ; for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1 ^ F2),d) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal (F1 ^ F2),d) * i,j = d
let d be Element of D; for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1 ^ F2),d) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal (F1 ^ F2),d) * i,j = d
let F1, F2 be FinSequence_of_Matrix of D; ( [i,j] in Indices (block_diagonal (F1 ^ F2),d) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) implies (block_diagonal (F1 ^ F2),d) * i,j = d )
set L1 = Len F1;
set W1 = Width F1;
set L2 = Len F2;
set W2 = Width F2;
set F12 = F1 ^ F2;
set L = Len (F1 ^ F2);
set W = Width (F1 ^ F2);
set B2 = block_diagonal F2,d;
set B12 = block_diagonal (F1 ^ F2),d;
A1:
dom (block_diagonal (F1 ^ F2),d) = Seg (len (block_diagonal (F1 ^ F2),d))
by FINSEQ_1:def 3;
A2:
len (Width F1) = len F1
by FINSEQ_1:def 18;
A3:
len (block_diagonal (F1 ^ F2),d) = Sum (Len (F1 ^ F2))
by Def5;
A4:
len F1 = len (Len F1)
by FINSEQ_1:def 18;
assume that
A5:
[i,j] in Indices (block_diagonal (F1 ^ F2),d)
and
A6:
( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) )
; (block_diagonal (F1 ^ F2),d) * i,j = d
i in dom (block_diagonal (F1 ^ F2),d)
by A5, ZFMISC_1:106;
then A7:
1 <= i
by FINSEQ_3:27;
A8:
(Width F1) ^ (Width F2) = Width (F1 ^ F2)
by Th18;
A9:
(Len F1) ^ (Len F2) = Len (F1 ^ F2)
by Th14;
then A10:
Sum (Len (F1 ^ F2)) = (Sum (Len F1)) + (Sum (Len F2))
by RVSUM_1:105;
per cases
( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) )
by A6;
suppose A11:
(
i <= Sum (Len F1) &
j > Sum (Width F1) )
;
(block_diagonal (F1 ^ F2),d) * i,j = dthen A12:
i in Seg (Sum (Len F1))
by A7, FINSEQ_1:3;
then
min (Len F1),
i in dom (Len F1)
by Def1;
then
min (Len F1),
i <= len (Len F1)
by FINSEQ_3:27;
then A13:
Sum ((Width (F1 ^ F2)) | (min (Len F1),i)) <= Sum ((Width (F1 ^ F2)) | (len (Len F1)))
by POLYNOM3:18;
A14:
(Width (F1 ^ F2)) | (len (Len F1)) = Width F1
by A8, A2, A4, FINSEQ_5:26;
min (Len (F1 ^ F2)),
i = min (Len F1),
i
by A9, A12, Th8;
then
Sum ((Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),i)) < j
by A11, A14, A13, XXREAL_0:2;
hence
(block_diagonal (F1 ^ F2),d) * i,
j = d
by A5, Def5;
verum end; suppose A15:
(
i > Sum (Len F1) &
j <= Sum (Width F1) )
;
(block_diagonal (F1 ^ F2),d) * i,j = dA16:
i in Seg (Sum (Len (F1 ^ F2)))
by A1, A3, A5, ZFMISC_1:106;
not
i in Seg (Sum (Len F1))
by A15, FINSEQ_1:3;
then A17:
i in (Seg ((Sum (Len F1)) + (Sum (Len F2)))) \ (Seg (Sum (Len F1)))
by A10, A16, XBOOLE_0:def 5;
then A18:
i -' (Sum (Len F1)) = i - (Sum (Len F1))
by Th9;
then A19:
i = (i -' (Sum (Len F1))) + (Sum (Len F1))
;
i -' (Sum (Len F1)) <> 0
by A15, A18;
then
i -' (Sum (Len F1)) in Seg (Sum (Len F2))
by A10, A16, A19, FINSEQ_1:82;
then
min (Len F2),
(i -' (Sum (Len F1))) in dom (Len F2)
by Def1;
then A20:
min (Len F2),
(i -' (Sum (Len F1))) >= 1
by FINSEQ_3:27;
min (Len (F1 ^ F2)),
i = (min (Len F2),(i -' (Sum (Len F1)))) + (len (Len F1))
by A9, A17, Th9;
then
(min (Len (F1 ^ F2)),i) -' 1
= ((min (Len F2),(i -' (Sum (Len F1)))) -' 1) + (len (Len F1))
by A20, NAT_D:38;
then
(min (Len (F1 ^ F2)),i) -' 1
>= (len (Len F1)) + 0
by XREAL_1:9;
then A21:
Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),i) -' 1)) >= Sum (((Width F1) ^ (Width F2)) | (len (Width F1)))
by A8, A2, A4, POLYNOM3:18;
((Width F1) ^ (Width F2)) | (len (Width F1)) = Width F1
by FINSEQ_5:26;
then
Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),i) -' 1)) >= j
by A15, A21, XXREAL_0:2;
hence
(block_diagonal (F1 ^ F2),d) * i,
j = d
by A5, Def5;
verum end;