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 ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),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 ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),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 ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),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 ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a)
let G be FinSequence_of_Matrix of K; :: thesis: ( i in Seg (width A) implies DelCol ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a) )
assume A1: i in Seg (width A) ; :: thesis: DelCol ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a)
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 BAG = block_diagonal (<*A,(block_diagonal (G,a))*>,a);
set BDG = block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a);
A2: len (DelCol (A,i)) = len A by MATRIX_0:def 13;
len (block_diagonal (<*A,(block_diagonal (G,a))*>,a)) = Sum (Len (<*A*> ^ <*(block_diagonal (G,a))*>)) by Def5;
then A3: len (block_diagonal (<*A,(block_diagonal (G,a))*>,a)) = (len A) + (len (block_diagonal (G,a))) by Th16;
A4: len (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) = Sum (Len (<*(DelCol (A,i))*> ^ <*(block_diagonal (G,a))*>)) by Def5;
then A5: len (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) = (len (DelCol (A,i))) + (len (block_diagonal (G,a))) by Th16;

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

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 (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) implies (DelCol ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) . j )
assume that
A7: 1 <= j and
A8: j <= len (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) ; :: thesis: (DelCol ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) . j
A9: j in Seg (len (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a))) by A7, A8;

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

per cases ( j <= len A or j > len A ) ;

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

then A12: j in Seg (len A) by A7;
A13: j in dom (DelCol (A,i)) by A2, A7, A11, FINSEQ_3:25;
A14: dom (Line (A,j)) = Seg (width A) by FINSEQ_2:124;
A15: j in dom A by A7, A11, FINSEQ_3:25;
then A16: Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),j) = (Line (A,j)) ^ ((width (block_diagonal (G,a))) |-> a) by Th23;
Del ((Line (A,j)),i) = Da9 . j by A15, MATRIX_0:def 13
.= Line ((DelCol (A,i)),j) by A2, A12, MATRIX_0:52 ;
hence Del ((Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),j)),i) = (Line ((DelCol (A,i)),j)) ^ ((width (block_diagonal (G,a))) |-> a) by A1, A16, A14, Th2
.= Line ((block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)),j) by A13, Th23
.= (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) . j by A4, A9, MATRIX_0:52 ;
:: thesis: verum

end;

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

then reconsider jL = j - (len A) as Element of NAT by NAT_1:21;
jL <> 0 by A17;
then A18: jL >= 1 by NAT_1:14;
width A <> 0 by A1;
then reconsider w1 = (width A) - 1 as Element of NAT by NAT_1:14, NAT_1:21;
A19: dom ((width A) |-> a) = Seg (width A) by FINSEQ_2:124;
A20: width (DelCol (A,i)) = (w1 + 1) -' 1 by A1, LAPLACE:3
.= w1 by NAT_D:34 ;
jL + (len A) <= (len (block_diagonal (G,a))) + (len A) by A5, A8, MATRIX_0:def 13;
then jL <= len (block_diagonal (G,a)) by XREAL_1:8;
then A21: jL in dom (block_diagonal (G,a)) by A18, FINSEQ_3:25;
then Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),(jL + (len A))) = ((width A) |-> a) ^ (Line ((block_diagonal (G,a)),jL)) by Th23;
hence Del ((Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),j)),i) = (Del (((w1 + 1) |-> a),i)) ^ (Line ((block_diagonal (G,a)),jL)) by A1, A19, Th2
.= ((width (DelCol (A,i))) |-> a) ^ (Line ((block_diagonal (G,a)),jL)) by A1, A20, Th4
.= Line ((block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)),((len A) + jL)) by A2, A21, Th23
.= (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) . j by A4, A9, MATRIX_0:52 ;
:: thesis: verum

end;

end;

end;

j in dom (block_diagonal (<*A,(block_diagonal (G,a))*>,a)) by A2, A5, A3, A7, A8, FINSEQ_3:25;
hence (DelCol ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a)) . j by A10, MATRIX_0:def 13; :: thesis: verum

end;

A22: block_diagonal ((<*(DelCol (A,i))*> ^ G),a) = block_diagonal (<*(DelCol (A,i)),(block_diagonal (G,a))*>,a) by Th36;
A23: len (DelCol ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) = len (block_diagonal (<*A,(block_diagonal (G,a))*>,a)) by MATRIX_0:def 13;
block_diagonal ((<*A*> ^ G),a) = block_diagonal (<*A,(block_diagonal (G,a))*>,a) by Th36;
hence DelCol ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a) by A2, A23, A4, A3, A6, A22, Th16, FINSEQ_1:14; :: thesis: verum