let i be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let K be Field; :: thesis: for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let a be Element of K; :: thesis: for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let A be Matrix of K; :: thesis: for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let G be FinSequence_of_Matrix of K; :: thesis: ( i in Seg (width A) implies DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a) )
assume A1: i in Seg (width A) ; :: thesis: DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
set iS = i + (Sum (Width G));
set bG = block_diagonal (G,a);
set Da = DelCol (A,i);
set AA = <*A*>;
set DA = <*(DelCol (A,i))*>;
set BG = <*(block_diagonal (G,a))*>;
set BGA = block_diagonal (<*(block_diagonal (G,a)),A*>,a);
set BGD = block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a);
A2: len (DelCol (A,i)) = len A by MATRIX_0:def 13;
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*A*>)) by Def5;
then A3: len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (len (block_diagonal (G,a))) + (len A) by Th16;
A4: width (block_diagonal (G,a)) = Sum (Width G) by Def5;
A5: len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*(DelCol (A,i))*>)) by Def5;
then A6: len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) = (len (block_diagonal (G,a))) + (len (DelCol (A,i))) by Th16;

A7: now :: thesis: for j being Nat st 1 <= j & j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) holds
(DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j

width A <> 0 by A1;
then width A >= 1 by NAT_1:14;
then (width A) -' 1 = (width A) - 1 by XREAL_1:233;
then A8: width A = ((width A) -' 1) + 1 ;
A9: dom ((width A) |-> a) = Seg (width A) by FINSEQ_2:124;
A10: len ((width (block_diagonal (G,a))) |-> a) = width (block_diagonal (G,a)) by CARD_1:def 7;
reconsider Da9 = DelCol (A,i) as Matrix of len (DelCol (A,i)), width (DelCol (A,i)),K by MATRIX_0:51;
let j be Nat; :: thesis: ( 1 <= j & j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) implies (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j )
assume that
A11: 1 <= j and
A12: j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) ; :: thesis: (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j
A13: j in Seg (len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a))) by A11, A12;
A14: len (Line ((block_diagonal (G,a)),j)) = width (block_diagonal (G,a)) by MATRIX_0:def 7;

A15: now :: thesis: Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j

per cases ( j <= len (block_diagonal (G,a)) or j > len (block_diagonal (G,a)) ) ;

suppose j <= len (block_diagonal (G,a)) ; :: thesis: Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j

then A16: j in dom (block_diagonal (G,a)) by A11, FINSEQ_3:25;
then Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j) = (Line ((block_diagonal (G,a)),j)) ^ ((width A) |-> a) by Th23;
hence Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (Line ((block_diagonal (G,a)),j)) ^ (Del (((width A) |-> a),i)) by A1, A4, A9, A14, Th3
.= (Line ((block_diagonal (G,a)),j)) ^ (((width A) -' 1) |-> a) by A1, A8, Th4
.= (Line ((block_diagonal (G,a)),j)) ^ ((width (DelCol (A,i))) |-> a) by A1, LAPLACE:3
.= Line ((block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)),j) by A16, Th23
.= (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j by A5, A13, MATRIX_0:52 ;
:: thesis: verum

end;

suppose A17: j > len (block_diagonal (G,a)) ; :: thesis: Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j

then reconsider jL = j - (len (block_diagonal (G,a))) as Element of NAT by NAT_1:21;
jL <> 0 by A17;
then A18: jL >= 1 by NAT_1:14;
jL + (len (block_diagonal (G,a))) <= (len (block_diagonal (G,a))) + (len A) by A6, A12, MATRIX_0:def 13;
then A19: jL <= len A by XREAL_1:8;
then A20: jL in dom (DelCol (A,i)) by A2, A18, FINSEQ_3:25;
A21: jL in Seg (len A) by A18, A19;
A22: jL in dom A by A18, A19, FINSEQ_3:25;
then A23: Del ((Line (A,jL)),i) = Da9 . jL by MATRIX_0:def 13
.= Line ((DelCol (A,i)),jL) by A2, A21, MATRIX_0:52 ;
A24: dom (Line (A,jL)) = Seg (width A) by FINSEQ_2:124;
Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(jL + (len (block_diagonal (G,a))))) = ((width (block_diagonal (G,a))) |-> a) ^ (Line (A,jL)) by A22, Th23;
hence Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = ((width (block_diagonal (G,a))) |-> a) ^ (Del ((Line (A,jL)),i)) by A1, A4, A10, A24, Th3
.= Line ((block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)),((len (block_diagonal (G,a))) + jL)) by A20, A23, Th23
.= (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j by A5, A13, MATRIX_0:52 ;
:: thesis: verum

end;

end;

end;

j in dom (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) by A2, A6, A3, A11, A12, FINSEQ_3:25;
hence (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j by A15, MATRIX_0:def 13; :: thesis: verum

end;

A25: block_diagonal ((G ^ <*(DelCol (A,i))*>),a) = block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a) by Th35;
A26: len (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) = len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) by MATRIX_0:def 13;
block_diagonal ((G ^ <*A*>),a) = block_diagonal (<*(block_diagonal (G,a)),A*>,a) by Th35;
hence DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a) by A2, A26, A5, A3, A7, A25, Th16, FINSEQ_1:14; :: thesis: verum