let i be Nat; for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))
let D be non empty set ; for d being Element of D
for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))
let d be Element of D; for F being FinSequence_of_Matrix of D st i in dom F holds
F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))
let F be FinSequence_of_Matrix of D; ( i in dom F implies F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) )
assume A1:
i in dom F
; F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))
set L = Len F;
set Fi = F . i;
A2:
dom F = dom (Len F)
by Def3;
then A3:
len (F . i) = (Len F) . i
by A1, Def3;
set SL = Sum ((Len F) | i);
set SL1 = Sum ((Len F) | (i -' 1));
A4:
(Sum ((Len F) | (i -' 1))) + ((Len F) . i) = Sum ((Len F) | i)
by A1, A2, Lm2;
reconsider FI = F . i as Matrix of len (F . i), width (F . i),D by MATRIX_0:51;
set B = block_diagonal (F,d);
set W = Width F;
set SW1 = Sum ((Width F) | (i -' 1));
set SW = Sum ((Width F) | i);
A5:
dom F = dom (Width F)
by Def4;
then A6:
(Sum ((Width F) | (i -' 1))) + ((Width F) . i) = Sum ((Width F) | i)
by A1, Lm2;
Sum ((Len F) | (i -' 1)) <= Sum ((Len F) | i)
by NAT_D:35, POLYNOM3:18;
then
Seg (Sum ((Len F) | (i -' 1))) c= Seg (Sum ((Len F) | i))
by FINSEQ_1:5;
then A7: card ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))) =
(card (Seg (Sum ((Len F) | i)))) - (card (Seg (Sum ((Len F) | (i -' 1)))))
by CARD_2:44
.=
(Sum ((Len F) | i)) - (card (Seg (Sum ((Len F) | (i -' 1)))))
by FINSEQ_1:57
.=
((Sum ((Len F) | (i -' 1))) + ((Len F) . i)) - (Sum ((Len F) | (i -' 1)))
by A4, FINSEQ_1:57
.=
len (F . i)
by A1, A2, Def3
;
Sum ((Width F) | (i -' 1)) <= Sum ((Width F) | i)
by NAT_D:35, POLYNOM3:18;
then
Seg (Sum ((Width F) | (i -' 1))) c= Seg (Sum ((Width F) | i))
by FINSEQ_1:5;
then A8: card ((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))) =
(card (Seg (Sum ((Width F) | i)))) - (card (Seg (Sum ((Width F) | (i -' 1)))))
by CARD_2:44
.=
(Sum ((Width F) | i)) - (card (Seg (Sum ((Width F) | (i -' 1)))))
by FINSEQ_1:57
.=
((Sum ((Width F) | (i -' 1))) + ((Width F) . i)) - (Sum ((Width F) | (i -' 1)))
by A6, FINSEQ_1:57
.=
width (F . i)
by A1, A5, Def4
;
A9:
width (F . i) = (Width F) . i
by A1, A5, Def4;
now for j, k being Nat st [j,k] in Indices FI holds
(Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))) * (j,k) = (F . i) * (j,k)A10:
Indices FI = Indices (Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))))
by A7, A8, MATRIX_0:26;
A11:
dom FI = Seg ((Len F) . i)
by A3, FINSEQ_1:def 3;
let j,
k be
Nat;
( [j,k] in Indices FI implies (Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))) * (j,k) = (F . i) * (j,k) )assume A12:
[j,k] in Indices FI
;
(Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))) * (j,k) = (F . i) * (j,k)
k in Seg ((Width F) . i)
by A9, A12, ZFMISC_1:87;
then A13:
(Sgm ((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1)))))) . k = k + (Sum ((Width F) | (i -' 1)))
by A6, MATRIX15:8;
j in dom FI
by A12, ZFMISC_1:87;
then
(Sgm ((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1)))))) . j = j + (Sum ((Len F) | (i -' 1)))
by A4, A11, MATRIX15:8;
hence (Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))) * (
j,
k) =
(block_diagonal (F,d)) * (
(j + (Sum ((Len F) | (i -' 1)))),
(k + (Sum ((Width F) | (i -' 1)))))
by A12, A10, A13, MATRIX13:def 1
.=
(F . i) * (
j,
k)
by A1, A12, Th30
;
verum end;
hence
F . i = Segm ((block_diagonal (F,d)),((Seg (Sum ((Len F) | i))) \ (Seg (Sum ((Len F) | (i -' 1))))),((Seg (Sum ((Width F) | i))) \ (Seg (Sum ((Width F) | (i -' 1))))))
by A7, A8, MATRIX_0:27; verum