let i, j be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( [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:
( (Width F1) ^ (Width F2) = Width (F1 ^ F2) & (Len F1) ^ (Len F2) = Len (F1 ^ F2) )
by Th14, Th18;
then A2:
Sum (Len (F1 ^ F2)) = (Sum (Len F1)) + (Sum (Len F2))
by RVSUM_1:105;
A3:
( dom (block_diagonal (F1 ^ F2),d) = Seg (len (block_diagonal (F1 ^ F2),d)) & len (block_diagonal (F1 ^ F2),d) = Sum (Len (F1 ^ F2)) & len (Width F1) = len F1 & len F1 = len (Len F1) )
by Def5, FINSEQ_1:def 3, FINSEQ_1:def 18;
assume that
A4:
[i,j] in Indices (block_diagonal (F1 ^ F2),d)
and
A5:
( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) )
; :: thesis: (block_diagonal (F1 ^ F2),d) * i,j = d
i in dom (block_diagonal (F1 ^ F2),d)
by A4, ZFMISC_1:106;
then A6:
1 <= i
by FINSEQ_3:27;
per cases
( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) )
by A5;
suppose A7:
(
i <= Sum (Len F1) &
j > Sum (Width F1) )
;
:: thesis: (block_diagonal (F1 ^ F2),d) * i,j = dthen
i in Seg (Sum (Len F1))
by A6, FINSEQ_1:3;
then A8:
(
min (Len (F1 ^ F2)),
i = min (Len F1),
i &
min (Len F1),
i in dom (Len F1) )
by A1, Th8, Def1;
then
min (Len F1),
i <= len (Len F1)
by FINSEQ_3:27;
then
(
(Width (F1 ^ F2)) | (len (Len F1)) = Width F1 &
Sum ((Width (F1 ^ F2)) | (min (Len F1),i)) <= Sum ((Width (F1 ^ F2)) | (len (Len F1))) )
by A1, A3, FINSEQ_5:26, POLYNOM3:18;
then
Sum ((Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),i)) < j
by A8, A7, XXREAL_0:2;
hence
(block_diagonal (F1 ^ F2),d) * i,
j = d
by A4, Def5;
:: thesis: verum end; suppose A9:
(
i > Sum (Len F1) &
j <= Sum (Width F1) )
;
:: thesis: (block_diagonal (F1 ^ F2),d) * i,j = dthen A10:
( not
i in Seg (Sum (Len F1)) &
i in Seg (Sum (Len (F1 ^ F2))) )
by A4, A3, FINSEQ_1:3, ZFMISC_1:106;
then
i in (Seg ((Sum (Len F1)) + (Sum (Len F2)))) \ (Seg (Sum (Len F1)))
by A2, XBOOLE_0:def 5;
then A11:
(
min (Len (F1 ^ F2)),
i = (min (Len F2),(i -' (Sum (Len F1)))) + (len (Len F1)) &
i -' (Sum (Len F1)) = i - (Sum (Len F1)) )
by A1, Th9;
then A12:
(
i = (i -' (Sum (Len F1))) + (Sum (Len F1)) &
i -' (Sum (Len F1)) <> 0 )
by A9;
i -' (Sum (Len F1)) in Seg (Sum (Len F2))
by A2, A10, A12, FINSEQ_1:82;
then
min (Len F2),
(i -' (Sum (Len F1))) in dom (Len F2)
by Def1;
then
min (Len F2),
(i -' (Sum (Len F1))) >= 1
by FINSEQ_3:27;
then
(min (Len (F1 ^ F2)),i) -' 1
= ((min (Len F2),(i -' (Sum (Len F1)))) -' 1) + (len (Len F1))
by A11, NAT_D:38;
then
(min (Len (F1 ^ F2)),i) -' 1
>= (len (Len F1)) + 0
by XREAL_1:9;
then
(
Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),i) -' 1)) >= Sum (((Width F1) ^ (Width F2)) | (len (Width F1))) &
((Width F1) ^ (Width F2)) | (len (Width F1)) = Width F1 )
by A1, A3, FINSEQ_5:26, POLYNOM3:18;
then
Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),i) -' 1)) >= j
by A9, XXREAL_0:2;
hence
(block_diagonal (F1 ^ F2),d) * i,
j = d
by A4, Def5;
:: thesis: verum end;