let i, j, n 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 ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),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 ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),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 ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),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 ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a)
let A be Matrix of n,K; :: thesis: ( i in dom A & j in Seg n implies Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a) )
assume that
A1: i in dom A and
A2: j in Seg n ; :: thesis: Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a)
n <> 0 by A2;
then A3: n >= 1 by NAT_1:14;
set AA = <*A*>;
set b = block_diagonal (R,a);
set B = <*(block_diagonal (R,a))*>;
set LAR = Sum (Len (<*A*> ^ R));
set LAB = Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>));
A4: width A = n by MATRIX_0:24;
Width <*A*> = <*(width A)*> by Th19;
then A5: Sum (Width <*A*>) = width A by RVSUM_1:73;
A6: Width <*(block_diagonal (R,a))*> = <*(width (block_diagonal (R,a)))*> by Th19;
A7: Len <*A*> = <*(len A)*> by Th15;
then A8: Sum (Len <*A*>) = len A by RVSUM_1:73;
Len (<*A*> ^ <*(block_diagonal (R,a))*>) = (Len <*A*>) ^ (Len <*(block_diagonal (R,a))*>) by Th14;
then A9: Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>)) = (len A) + (Sum (Len <*(block_diagonal (R,a))*>)) by A7, RVSUM_1:76;
A10: Len (<*A*> ^ <*(block_diagonal (R,a))*>) = Width (<*A*> ^ <*(block_diagonal (R,a))*>) by Th46;
Width (<*A*> ^ <*(block_diagonal (R,a))*>) = (Width <*A*>) ^ (Width <*(block_diagonal (R,a))*>) by Th18;
then A11: Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>)) = (Sum (Width <*A*>)) + (width (block_diagonal (R,a))) by A6, A10, RVSUM_1:74;
Len <*(block_diagonal (R,a))*> = <*(len (block_diagonal (R,a)))*> by Th15;
then A12: Sum (Len <*(block_diagonal (R,a))*>) = len (block_diagonal (R,a)) by RVSUM_1:73;
A13: len A = n by MATRIX_0:24;
then A14: dom A = Seg n by FINSEQ_1:def 3;

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

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

then A16: i = 1 by A1, A14, FINSEQ_1:2, TARSKI:def 1;
A17: j = 1 by A2, A15, FINSEQ_1:2, TARSKI:def 1;
len (Deleting (A,i,j)) = 1 -' 1 by A1, A15, LAPLACE:2
.= 0 by XREAL_1:232 ;
then A18: Deleting (A,i,j) = {} ;
thus Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = Deleting ((block_diagonal ((<*A*> ^ <*(block_diagonal (R,a))*>),a)),i,j) by Th36
.= Segm ((block_diagonal ((<*A*> ^ <*(block_diagonal (R,a))*>),a)),((Seg (Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>)))) \ {i}),((Seg (Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>)))) \ {j})) by MATRIX13:58
.= block_diagonal (R,a) by A13, A4, A9, A11, A12, A8, A5, A15, A16, A17, Th33, FINSEQ_1:2
.= block_diagonal (<*(block_diagonal (R,a))*>,a) by Th34
.= block_diagonal ((<*(Deleting (A,i,j))*> ^ <*(block_diagonal (R,a))*>),a) by A18, Th40
.= block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a) by Th36 ; :: thesis: verum

end;

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

then A19: width A = width (DelLine (A,i)) by A13, LAPLACE:4;
thus Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = DelCol ((DelLine ((block_diagonal ((<*A*> ^ R),a)),i)),j)
.= DelCol ((block_diagonal ((<*(DelLine (A,i))*> ^ R),a)),j) by A1, A19, Th41
.= block_diagonal ((<*(DelCol ((DelLine (A,i)),j))*> ^ R),a) by A2, A4, A19, Th43
.= block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a) ; :: thesis: verum

end;

end;