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 A1: ( i in Seg (Sum (Len F)) & 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;
A2: ( 1 <= i & i <= Sum ((Len F) | m) & Sum ((Len F) | (m -' 1)) < i ) by A1, Def1, Th7, FINSEQ_1:3;
then A3: ( i - (Sum ((Len F) | (m -' 1))) = i -' (Sum ((Len F) | (m -' 1))) & i - (Sum ((Len F) | (m -' 1))) <> 0 ) by XREAL_1:235;
then A4: i -' (Sum ((Len F) | (m -' 1))) >= 1 by NAT_1:14;
A5: ( m in dom (Len F) & dom (Len F) = dom F ) by A1, Def1, Def3;
then ( 1 <= m & m <= len F & m <= len (Len F) ) by FINSEQ_3:27;
then A6: ( m -' 1 = m - 1 & len (F | m) = m & len ((Len F) | m) = m ) by FINSEQ_1:80, XREAL_1:235;
then A7: m = (m -' 1) + 1 ;
then A8: ( F | m = ((F | m) | (m -' 1)) ^ <*((F | m) . m)*> & (F | m) . m = F . m & F = (F | m) ^ (F /^ m) & (Len F) | m = (((Len F) | m) | (m -' 1)) ^ <*(((Len F) | m) . m)*> & ((Len F) | m) . m = (Len F) . m ) by A6, FINSEQ_3:61, FINSEQ_3:121, RFINSEQ:21;
m -' 1 <= m by A7, NAT_1:11;
then Seg (m -' 1) c= Seg m by FINSEQ_1:7;
then A9: ( (F | m) | (m -' 1) = F | (m -' 1) & ((Len F) | m) | (m -' 1) = (Len F) | (m -' 1) ) by RELAT_1:103;
set BFm = block_diagonal (F | m),d;
set BFm1 = block_diagonal (F | (m -' 1)),d;
Sum ((Len F) | m) = (Sum ((Len F) | (m -' 1))) + ((Len F) . m) by A8, A9, RVSUM_1:104
.= (Sum ((Len F) | (m -' 1))) + (len (F . m)) by A5, Def3 ;
then (len (F . m)) + (Sum ((Len F) | (m -' 1))) >= (i -' (Sum ((Len F) | (m -' 1)))) + (Sum ((Len F) | (m -' 1))) by A3, A1, Def1;
then len (F . m) >= i -' (Sum ((Len F) | (m -' 1))) by XREAL_1:8;
then A10: i -' (Sum ((Len F) | (m -' 1))) in dom (F . m) by A4, FINSEQ_3:27;
A11: len (block_diagonal (F | (m -' 1)),d) = Sum (Len (F | (m -' 1))) by Def5
.= Sum ((Len F) | (m -' 1)) by Th17 ;
A12: width (block_diagonal (F | (m -' 1)),d) = Sum (Width (F | (m -' 1))) by Def5
.= Sum ((Width F) | (m -' 1)) by Th21 ;
block_diagonal (F | m),d = block_diagonal <*(block_diagonal (F | (m -' 1)),d),(F . m)*>,d by A9, A8, Th35;
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 A10, A11, A12, Th23
.= Line (block_diagonal (F | m),d),i by A3 ;
then A13: Line (block_diagonal (F | m),d),i = ((Sum (Width (F | (m -' 1)))) |-> d) ^ (Line (F . m),(i -' (Sum ((Len F) | (m -' 1))))) by Th21;
set BF'm = block_diagonal (F /^ m),d;
A14: block_diagonal F,d = block_diagonal ((F | m) ^ <*(block_diagonal (F /^ m),d)*>),d by A8, Th36
.= block_diagonal <*(block_diagonal (F | m),d),(block_diagonal (F /^ m),d)*>,d by Th35 ;
Sum (Width F) = width (block_diagonal <*(block_diagonal (F | m),d),(block_diagonal (F /^ m),d)*>,d) by A14, 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 A15: (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:235
.= width (block_diagonal (F /^ m),d) ;
len (block_diagonal (F | m),d) = Sum (Len (F | m)) by Def5
.= Sum ((Len F) | m) by Th17 ;
then i in dom (block_diagonal (F | m),d) by A2, FINSEQ_3:27;
then Line (block_diagonal F,d),i = (Line (block_diagonal (F | m),d),i) ^ ((width (block_diagonal (F /^ m),d)) |-> d) by A14, Th23;
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 A15, A13, Th17; :: thesis: verum