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

width A <> 0 by A1, NAT_1:14;
then width A >= 1 by A1, NAT_1:14;
then (width A) -' 1 = (width A) - 1 by A1, FINSEQ_1:4, NAT_1:14, XREAL_1:235;
then A8: width A = ((width A) -' 1) + 1 ;
A9: dom ((width A) |-> a) = Seg (width A) by FINSEQ_2:144;
A10: len ((width (block_diagonal G,a)) |-> a) = width (block_diagonal G,a) by FINSEQ_1:def 18;
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 <*(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, FINSEQ_1:3;
A14: len (Line (block_diagonal G,a),j) = width (block_diagonal G,a) by MATRIX_1:def 8;

A15: now

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:27;
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_2:10 ;
:: 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_2:def 6;
then A19: jL <= len A by XREAL_1:10;
then A20: jL in dom (DelCol A,i) by A2, A18, FINSEQ_3:27;
A21: jL in Seg (len A) by A18, A19;
A22: jL in dom A by A18, A19, FINSEQ_3:27;
then A23: Del (Line A,jL),i = Da9 . jL by MATRIX_2:def 6
.= Line (DelCol A,i),jL by A2, A21, MATRIX_2:10 ;
A24: dom (Line A,jL) = Seg (width A) by FINSEQ_2:144;
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_2:10 ;
:: thesis: verum

end;

end;

end;

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