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 dom A & width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (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 dom A & width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (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 dom A & width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
let A be Matrix of K; :: thesis: for G being FinSequence_of_Matrix of K st i in dom A & width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
let G be FinSequence_of_Matrix of K; :: thesis: ( i in dom A & width A = width (DelLine (A,i)) implies DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a) )
assume that
A1: i in dom A and
A2: width A = width (DelLine (A,i)) ; :: thesis: DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
A3: i in Seg (len A) by A1, FINSEQ_1:def 3;
set da = DelLine (A,i);
consider m being Nat such that
A4: len A = m + 1 and
A5: len (DelLine (A,i)) = m by A1, FINSEQ_3:104;
set Si = (Sum (Len G)) + i;
set bG = block_diagonal (G,a);
set DA = <*(DelLine (A,i))*>;
set AA = <*A*>;
set BG = <*(block_diagonal (G,a))*>;
set bGA = block_diagonal (<*(block_diagonal (G,a)),A*>,a);
set bGdA = block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a);
A6: Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))) = dom (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) by FINSEQ_1:def 3;
A7: len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*(DelLine (A,i))*>)) by Def5;
then A8: len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = m + (len (block_diagonal (G,a))) by A5, Th16;
A9: len (block_diagonal (G,a)) = Sum (Len G) by Def5;
A10: len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*A*>)) by Def5;
then A11: len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (len A) + (len (block_diagonal (G,a))) by Th16;
then A12: len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (m + (len (block_diagonal (G,a)))) + 1 by A4;
A13: len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = (len (DelLine (A,i))) + (len (block_diagonal (G,a))) by A7, Th16;

A14: now :: thesis: for j being Nat st 1 <= j & j <= m + (len (block_diagonal (G,a))) holds
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j

m + (len (block_diagonal (G,a))) <= len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) by A12, NAT_1:11;
then A15: Seg (m + (len (block_diagonal (G,a)))) c= Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))) by FINSEQ_1:5;
reconsider da9 = DelLine (A,i) as Matrix of len (DelLine (A,i)), width (DelLine (A,i)),K by MATRIX_0:51;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
let j be Nat; :: thesis: ( 1 <= j & j <= m + (len (block_diagonal (G,a))) implies (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j )
assume that
A16: 1 <= j and
A17: j <= m + (len (block_diagonal (G,a))) ; :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j
A18: j in Seg (m + (len (block_diagonal (G,a)))) by A16, A17;
A19: 1 <= 1 + j by NAT_1:11;
j + 1 <= len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) by A12, A17, XREAL_1:7;
then A20: j + 1 in Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))) by A19;

now :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j

per cases ( j <= len (block_diagonal (G,a)) or j > len (block_diagonal (G,a)) ) ;

suppose A21: j <= len (block_diagonal (G,a)) ; :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j

then A22: j in dom (block_diagonal (G,a)) by A16, FINSEQ_3:25;
0 < i by A3;
then j + 0 < (len (block_diagonal (G,a))) + i by A21, XREAL_1:8;
then j < (Sum (Len G)) + i by Def5;
hence (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . j by FINSEQ_3:110
.= Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j) by A10, A18, A15, MATRIX_0:52
.= (Line ((block_diagonal (G,a)),j)) ^ ((width (DelLine (A,i))) |-> a) by A2, A22, Th23
.= Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),j) by A22, Th23
.= (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j by A5, A7, A13, A18, MATRIX_0:52 ;
:: thesis: verum

end;

suppose A23: j > len (block_diagonal (G,a)) ; :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j

then reconsider jL = j - (len (block_diagonal (G,a))) as Element of NAT by NAT_1:21;
A24: 0 + 1 <= jL + 1 by NAT_1:13;
jL + (len (block_diagonal (G,a))) <= m + (len (block_diagonal (G,a))) by A17;
then A25: jL <= m by XREAL_1:8;
then A26: jL + 1 <= len A by A4, XREAL_1:7;
then A27: jL + 1 in dom A by A24, FINSEQ_3:25;
jL <> 0 by A23;
then A28: 1 <= jL by NAT_1:14;
then A29: jL in dom (DelLine (A,i)) by A5, A25, FINSEQ_3:25;
A30: jL + 1 in Seg (len A) by A24, A26;
A31: jL in Seg (len (DelLine (A,i))) by A5, A28, A25;
A32: jL <= len A by A4, A25, NAT_1:13;
then A33: jL in Seg (len A) by A28;
A34: jL in dom A by A28, A32, FINSEQ_3:25;

now :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))

per cases ( j < (Sum (Len G)) + i or j >= (Sum (Len G)) + i ) ;

suppose A35: j < (Sum (Len G)) + i ; :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))

then jL + (len (block_diagonal (G,a))) < i + (len (block_diagonal (G,a))) by Def5;
then A36: jL < i by XREAL_1:7;
A37: Line (A,jL) = A9 . jL by A33, MATRIX_0:52
.= da9 . jL by A36, FINSEQ_3:110
.= Line ((DelLine (A,i)),jL) by A31, MATRIX_0:52 ;
thus (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . j by A35, FINSEQ_3:110
.= Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(jL + (len (block_diagonal (G,a))))) by A10, A18, A15, MATRIX_0:52
.= ((width (block_diagonal (G,a))) |-> a) ^ (Line ((DelLine (A,i)),jL)) by A34, A37, Th23
.= Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a))))) by A29, Th23 ; :: thesis: verum

end;

suppose A38: j >= (Sum (Len G)) + i ; :: thesis: (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))

then jL + (len (block_diagonal (G,a))) >= i + (len (block_diagonal (G,a))) by Def5;
then A39: jL >= i by XREAL_1:8;
A40: Line (A,(1 + jL)) = A9 . (1 + jL) by A30, MATRIX_0:52
.= da9 . jL by A1, A4, A25, A39, FINSEQ_3:111
.= Line ((DelLine (A,i)),jL) by A31, MATRIX_0:52 ;
thus (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . (j + 1) by A9, A11, A12, A3, A6, A17, A38, FINSEQ_1:60, FINSEQ_3:111
.= Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((jL + 1) + (len (block_diagonal (G,a))))) by A10, A20, MATRIX_0:52
.= ((width (block_diagonal (G,a))) |-> a) ^ (Line ((DelLine (A,i)),jL)) by A27, A40, Th23
.= Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a))))) by A29, Th23 ; :: thesis: verum

end;

end;

end;

hence (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j by A5, A7, A13, A18, MATRIX_0:52; :: thesis: verum

end;

end;

end;

hence (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j ; :: thesis: verum

end;

A41: block_diagonal ((G ^ <*(DelLine (A,i))*>),a) = block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a) by Th35;
A42: block_diagonal ((G ^ <*A*>),a) = block_diagonal (<*(block_diagonal (G,a)),A*>,a) by Th35;
len (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) = m + (len (block_diagonal (G,a))) by A9, A11, A12, A3, A6, FINSEQ_1:60, FINSEQ_3:109;
hence DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a) by A8, A42, A41, A14; :: thesis: verum