let n, i, j be Nat; :: thesis: for K being Field
for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let K be Field; :: thesis: for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let a be Element of K; :: thesis: for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let R be FinSequence_of_Square-Matrix of K; :: thesis: for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let A be Matrix of n,K; :: thesis: ( i in dom A & j in Seg n implies Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a )
assume that
A1: i in dom A and
A2: j in Seg n ; :: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
n <> 0 by A2;
then A3: n >= 1 by A2, FINSEQ_1:4, NAT_1:14;
set jS = j + (Sum (Len R));
set iS = i + (Sum (Len R));
set AA = <*A*>;
set b = block_diagonal R,a;
set B = <*(block_diagonal R,a)*>;
set LRA = Sum (Len (R ^ <*A*>));
set LBA = Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>));
A4: width A = n by MATRIX_1:25;
A5: Len R = Width R by Th46;
A6: len A = n by MATRIX_1:25;
then A7: dom A = Seg n by FINSEQ_1:def 3;
A8: Width <*A*> = <*(width A)*> by Th19;
A9: len (block_diagonal R,a) = Sum (Len R) by Def5;
A10: Len (<*(block_diagonal R,a)*> ^ <*A*>) = Width (<*(block_diagonal R,a)*> ^ <*A*>) by Th46;
A11: Len <*A*> = <*(len A)*> by Th15;
then A12: Sum (Len <*A*>) = len A by RVSUM_1:103;
Len (R ^ <*A*>) = (Len R) ^ (Len <*A*>) by Th14;
then A13: Sum (Len (R ^ <*A*>)) = (len A) + (Sum (Len R)) by A11, RVSUM_1:104;
Len (<*(block_diagonal R,a)*> ^ <*A*>) = (Len <*(block_diagonal R,a)*>) ^ (Len <*A*>) by Th14;
then A14: Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)) = (len A) + (Sum (Len <*(block_diagonal R,a)*>)) by A11, RVSUM_1:104;
A15: Width <*(block_diagonal R,a)*> = <*(width (block_diagonal R,a))*> by Th19;
then A16: Sum (Width <*(block_diagonal R,a)*>) = width (block_diagonal R,a) by RVSUM_1:103;
Width (<*(block_diagonal R,a)*> ^ <*A*>) = (Width <*(block_diagonal R,a)*>) ^ (Width <*A*>) by Th18;
then A17: Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)) = (Sum (Width <*A*>)) + (width (block_diagonal R,a)) by A15, A10, RVSUM_1:106;
Len <*(block_diagonal R,a)*> = <*(len (block_diagonal R,a))*> by Th15;
then A18: Sum (Len <*(block_diagonal R,a)*>) = len (block_diagonal R,a) by RVSUM_1:103;

per cases ( n = 1 or n > 1 ) by A3, XXREAL_0:1;

suppose A19: n = 1 ; :: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a

then A20: i = 1 by A1, A7, FINSEQ_1:4, TARSKI:def 1;
A21: j = 1 by A2, A19, FINSEQ_1:4, TARSKI:def 1;
len (Deleting A,i,j) = 1 -' 1 by A1, A19, LAPLACE:2
.= 0 by XREAL_1:234 ;
then A22: Deleting A,i,j = {} ;
thus Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = Deleting (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) by A9, A13, A14, A18, Th35
.= Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(i + (Sum (Len R)))}),((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(j + (Sum (Len R)))}) by MATRIX13:58
.= Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),(Seg (Sum (Len <*(block_diagonal R,a)*>))),((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(j + (Sum (Len R)))}) by A6, A9, A14, A18, A19, A20, FINSEQ_1:12
.= Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),(Seg (Sum (Len <*(block_diagonal R,a)*>))),(Seg (Sum (Width <*(block_diagonal R,a)*>))) by A6, A4, A9, A11, A8, A14, A17, A18, A12, A16, A19, A21, FINSEQ_1:12
.= block_diagonal R,a by A18, A16, Th32
.= block_diagonal <*(block_diagonal R,a)*>,a by Th34
.= block_diagonal (<*(block_diagonal R,a)*> ^ <*(Deleting A,i,j)*>),a by A22, Th40
.= block_diagonal (R ^ <*(Deleting A,i,j)*>),a by Th35 ; :: thesis: verum

end;

suppose n > 1 ; :: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a

then A23: width A = width (DelLine A,i) by A6, LAPLACE:4;
thus Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = DelCol (DelLine (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R)))),(j + (Sum (Len R))) by MATRIX_2:def 8
.= DelCol (block_diagonal (R ^ <*(DelLine A,i)*>),a),(j + (Sum (Len R))) by A1, A23, Th42
.= block_diagonal (R ^ <*(DelCol (DelLine A,i),j)*>),a by A2, A4, A5, A23, Th44
.= block_diagonal (R ^ <*(Deleting A,i,j)*>),a by MATRIX_2:def 8 ; :: thesis: verum

end;

end;