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_2:def 6;
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

reconsider Da9 = DelCol A,i as Matrix of len (DelCol A,i), width (DelCol A,i),K by MATRIX_2:7;
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, FINSEQ_1:3;

A10: now

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, FINSEQ_1:3;
A13: j in dom (DelCol A,i) by A2, A7, A11, FINSEQ_3:27;
A14: dom (Line A,j) = Seg (width A) by FINSEQ_2:144;
A15: j in dom A by A7, A11, FINSEQ_3:27;
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_2:def 6
.= Line (DelCol A,i),j by A2, A12, MATRIX_2:10 ;
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_2:10 ;
:: 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:144;
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_2:def 6;
then jL <= len (block_diagonal G,a) by XREAL_1:10;
then A21: jL in dom (block_diagonal G,a) by A18, FINSEQ_3:27;
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_2:10 ;
:: thesis: verum

end;

end;

end;

j in dom (block_diagonal <*A,(block_diagonal G,a)*>,a) by A2, A5, A3, A7, A8, FINSEQ_3:27;
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_2:def 6; :: 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_2:def 6;
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:18; :: thesis: verum