let i, m be Nat; :: thesis: for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in Seg (Sum (Len F)) & m = min ((Len F),i) holds
Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d)
let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence_of_Matrix of D st i in Seg (Sum (Len F)) & m = min ((Len F),i) holds
Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d)
let d be Element of D; :: thesis: for F being FinSequence_of_Matrix of D st i in Seg (Sum (Len F)) & m = min ((Len F),i) holds
Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d)
let F be FinSequence_of_Matrix of D; :: thesis: ( i in Seg (Sum (Len F)) & m = min ((Len F),i) implies Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d) )
assume that
A1: i in Seg (Sum (Len F)) and
A2: m = min ((Len F),i) ; :: thesis: Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d)
set L = Len F;
A3: ((Len F) | m) . m = (Len F) . m by FINSEQ_3:112;
set BF9m = block_diagonal ((F /^ m),d);
set BFm = block_diagonal ((F | m),d);
A4: len (block_diagonal ((F | m),d)) = Sum (Len (F | m)) by Def5
.= Sum ((Len F) | m) by Th17 ;
F = (F | m) ^ (F /^ m) by RFINSEQ:8;
then A5: block_diagonal (F,d) = block_diagonal (((F | m) ^ <*(block_diagonal ((F /^ m),d))*>),d) by Th36
.= block_diagonal (<*(block_diagonal ((F | m),d)),(block_diagonal ((F /^ m),d))*>,d) by Th35 ;
then Sum (Width F) = width (block_diagonal (<*(block_diagonal ((F | m),d)),(block_diagonal ((F /^ m),d))*>,d)) by Def5
.= Sum (Width <*(block_diagonal ((F | m),d)),(block_diagonal ((F /^ m),d))*>) by Def5
.= (width (block_diagonal ((F | m),d))) + (width (block_diagonal ((F /^ m),d))) by Th20
.= (Sum (Width (F | m))) + (width (block_diagonal ((F /^ m),d))) by Def5 ;
then A6: (Sum (Width F)) -' (Sum (Width (F | m))) = ((Sum (Width (F | m))) + (width (block_diagonal ((F /^ m),d)))) - (Sum (Width (F | m))) by NAT_1:11, XREAL_1:233
.= width (block_diagonal ((F /^ m),d)) ;
Sum ((Len F) | (m -' 1)) < i by A1, A2, Th7;
then A7: i - (Sum ((Len F) | (m -' 1))) = i -' (Sum ((Len F) | (m -' 1))) by XREAL_1:233;
A8: m in dom (Len F) by A1, A2, Def1;
then 1 <= m by FINSEQ_3:25;
then m -' 1 = m - 1 by XREAL_1:233;
then A9: m = (m -' 1) + 1 ;
then m -' 1 <= m by NAT_1:11;
then A10: Seg (m -' 1) c= Seg m by FINSEQ_1:5;
then A11: (F | m) | (m -' 1) = F | (m -' 1) by RELAT_1:74;
m <= len (Len F) by A8, FINSEQ_3:25;
then len ((Len F) | m) = m by FINSEQ_1:59;
then A12: (Len F) | m = (((Len F) | m) | (m -' 1)) ^ <*(((Len F) | m) . m)*> by A9, FINSEQ_3:55;
((Len F) | m) | (m -' 1) = (Len F) | (m -' 1) by A10, RELAT_1:74;
then Sum ((Len F) | m) = (Sum ((Len F) | (m -' 1))) + ((Len F) . m) by A12, A3, RVSUM_1:74
.= (Sum ((Len F) | (m -' 1))) + (len (F . m)) by A8, Def3 ;
then (len (F . m)) + (Sum ((Len F) | (m -' 1))) >= (i -' (Sum ((Len F) | (m -' 1)))) + (Sum ((Len F) | (m -' 1))) by A1, A2, A7, Def1;
then A13: len (F . m) >= i -' (Sum ((Len F) | (m -' 1))) by XREAL_1:6;
i - (Sum ((Len F) | (m -' 1))) <> 0 by A1, A2, Th7;
then i -' (Sum ((Len F) | (m -' 1))) >= 1 by A7, NAT_1:14;
then A14: i -' (Sum ((Len F) | (m -' 1))) in dom (F . m) by A13, FINSEQ_3:25;
set BFm1 = block_diagonal ((F | (m -' 1)),d);
A15: (F | m) . m = F . m by FINSEQ_3:112;
A16: width (block_diagonal ((F | (m -' 1)),d)) = Sum (Width (F | (m -' 1))) by Def5
.= Sum ((Width F) | (m -' 1)) by Th21 ;
A17: 1 <= i by A1, FINSEQ_1:1;
i <= Sum ((Len F) | m) by A1, A2, Def1;
then i in dom (block_diagonal ((F | m),d)) by A17, A4, FINSEQ_3:25;
then A18: Line ((block_diagonal (F,d)),i) = (Line ((block_diagonal ((F | m),d)),i)) ^ ((width (block_diagonal ((F /^ m),d))) |-> d) by A5, Th23;
dom (Len F) = dom F by Def3;
then m <= len F by A8, FINSEQ_3:25;
then len (F | m) = m by FINSEQ_1:59;
then F | m = ((F | m) | (m -' 1)) ^ <*((F | m) . m)*> by A9, FINSEQ_3:55;
then A19: block_diagonal ((F | m),d) = block_diagonal (<*(block_diagonal ((F | (m -' 1)),d)),(F . m)*>,d) by A15, A11, Th35;
len (block_diagonal ((F | (m -' 1)),d)) = Sum (Len (F | (m -' 1))) by Def5
.= Sum ((Len F) | (m -' 1)) by Th17 ;
then ((Sum ((Width F) | (m -' 1))) |-> d) ^ (Line ((F . m),(i -' (Sum ((Len F) | (m -' 1)))))) = Line ((block_diagonal ((F | m),d)),((Sum ((Len F) | (m -' 1))) + (i -' (Sum ((Len F) | (m -' 1)))))) by A14, A16, A19, Th23
.= Line ((block_diagonal ((F | m),d)),i) by A7 ;
then Line ((block_diagonal ((F | m),d)),i) = ((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum ((Len F) | (m -' 1)))))) by Th21;
hence Line ((block_diagonal (F,d)),i) = (((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line ((F . m),(i -' (Sum (Len (F | (m -' 1)))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> d) by A6, A18, Th17; :: thesis: verum