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:113;
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

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:7;
reconsider da9 = DelLine A,i as Matrix of len (DelLine A,i), width (DelLine A,i),K by MATRIX_2:7;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_2:7;
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, FINSEQ_1:3;
A19: 1 <= 1 + j by NAT_1:11;
j + 1 <= len (block_diagonal <*(block_diagonal G,a),A*>,a) by A12, A17, XREAL_1:9;
then A20: j + 1 in Seg (len (block_diagonal <*(block_diagonal G,a),A*>,a)) by A19;
A21: j in NAT by ORDINAL1:def 13;
A22: i in NAT by ORDINAL1:def 13;

now

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

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 A24: j in dom (block_diagonal G,a) by A16, FINSEQ_3:27;
0 < i by A3, FINSEQ_1:3;
then j + 0 < (len (block_diagonal G,a)) + i by A23, XREAL_1:10;
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 A12, A21, FINSEQ_3:119
.= Line (block_diagonal <*(block_diagonal G,a),A*>,a),j by A10, A18, A15, MATRIX_2:10
.= (Line (block_diagonal G,a),j) ^ ((width (DelLine A,i)) |-> a) by A2, A24, Th23
.= Line (block_diagonal <*(block_diagonal G,a),(DelLine A,i)*>,a),j by A24, Th23
.= (block_diagonal <*(block_diagonal G,a),(DelLine A,i)*>,a) . j by A5, A7, A13, A18, MATRIX_2:10 ;
:: thesis: verum

end;

suppose A25: 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;
A26: 0 + 1 <= jL + 1 by NAT_1:13;
jL + (len (block_diagonal G,a)) <= m + (len (block_diagonal G,a)) by A17;
then A27: jL <= m by XREAL_1:10;
then A28: jL + 1 <= len A by A4, XREAL_1:9;
then A29: jL + 1 in dom A by A26, FINSEQ_3:27;
jL <> 0 by A25;
then A30: 1 <= jL by NAT_1:14;
then A31: jL in dom (DelLine A,i) by A5, A27, FINSEQ_3:27;
A32: jL + 1 in Seg (len A) by A26, A28;
A33: jL in Seg (len (DelLine A,i)) by A5, A30, A27;
A34: jL <= len A by A4, A27, NAT_1:13;
then A35: jL in Seg (len A) by A30;
A36: jL in dom A by A30, A34, FINSEQ_3:27;

now

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

suppose A37: 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 A38: jL < i by XREAL_1:9;
A39: Line A,jL = A9 . jL by A35, MATRIX_2:10
.= da9 . jL by A4, A5, A22, A38, FINSEQ_3:119
.= Line (DelLine A,i),jL by A33, MATRIX_2:10 ;
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 A12, A21, A37, FINSEQ_3:119
.= Line (block_diagonal <*(block_diagonal G,a),A*>,a),(jL + (len (block_diagonal G,a))) by A10, A18, A15, MATRIX_2:10
.= ((width (block_diagonal G,a)) |-> a) ^ (Line (DelLine A,i),jL) by A36, A39, Th23
.= Line (block_diagonal <*(block_diagonal G,a),(DelLine A,i)*>,a),(jL + (len (block_diagonal G,a))) by A31, Th23 ; :: thesis: verum

end;

suppose A40: 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 A41: jL >= i by XREAL_1:10;
A42: Line A,(1 + jL) = A9 . (1 + jL) by A32, MATRIX_2:10
.= da9 . jL by A1, A4, A5, A27, A41, FINSEQ_3:120
.= Line (DelLine A,i),jL by A33, MATRIX_2:10 ;
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, A21, A40, FINSEQ_1:81, FINSEQ_3:120
.= Line (block_diagonal <*(block_diagonal G,a),A*>,a),((jL + 1) + (len (block_diagonal G,a))) by A10, A20, MATRIX_2:10
.= ((width (block_diagonal G,a)) |-> a) ^ (Line (DelLine A,i),jL) by A29, A42, Th23
.= Line (block_diagonal <*(block_diagonal G,a),(DelLine A,i)*>,a),(jL + (len (block_diagonal G,a))) by A31, 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_2:10; :: 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;

A43: block_diagonal (G ^ <*(DelLine A,i)*>),a = block_diagonal <*(block_diagonal G,a),(DelLine A,i)*>,a by Th35;
A44: 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:81, FINSEQ_3:118;
hence DelLine (block_diagonal (G ^ <*A*>),a),((Sum (Len G)) + i) = block_diagonal (G ^ <*(DelLine A,i)*>),a by A8, A44, A43, A14, FINSEQ_1:18; :: thesis: verum