let i, j be Nat; :: thesis: for D being non empty set
for d being Element of D
for F2, F1 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F2,d) holds
(block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))
let D be non empty set ; :: thesis: for d being Element of D
for F2, F1 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F2,d) holds
(block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))
let d be Element of D; :: thesis: for F2, F1 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal F2,d) holds
(block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))
let F2, F1 be FinSequence_of_Matrix of D; :: thesis: ( [i,j] in Indices (block_diagonal F2,d) implies (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1))) )
set L1 = Len F1;
set W1 = Width F1;
set L2 = Len F2;
set W2 = Width F2;
set F12 = F1 ^ F2;
set L = Len (F1 ^ F2);
set W = Width (F1 ^ F2);
set B2 = block_diagonal F2,d;
set B12 = block_diagonal (F1 ^ F2),d;
A1: ( (Width F1) ^ (Width F2) = Width (F1 ^ F2) & (Len F1) ^ (Len F2) = Len (F1 ^ F2) ) by Th14, Th18;
then A2: Sum (Len (F1 ^ F2)) = (Sum (Len F1)) + (Sum (Len F2)) by RVSUM_1:105;
A3: ( dom (block_diagonal (F1 ^ F2),d) = Seg (len (block_diagonal (F1 ^ F2),d)) & len (block_diagonal (F1 ^ F2),d) = Sum (Len (F1 ^ F2)) & len (Width F1) = len F1 & len F1 = len (Len F1) & len (block_diagonal F2,d) = Sum (Len F2) & len (Len F2) = len F2 ) by Def5, FINSEQ_1:def 3, FINSEQ_1:def 18;
assume A4: [i,j] in Indices (block_diagonal F2,d) ; :: thesis: (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))
then A5: ( i > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal (F1 ^ F2),d) & i in dom (block_diagonal F2,d) ) by Th27, ZFMISC_1:106;
then A6: ( i + (Sum (Len F1)) in dom (block_diagonal (F1 ^ F2),d) & i in Seg (len (block_diagonal F2,d)) & i + (Sum (Len F1)) > 0 + (Sum (Len F1)) ) by FINSEQ_1:def 3, XREAL_1:8, ZFMISC_1:106;
then ( not i + (Sum (Len F1)) in Seg (Sum (Len F1)) & min (Len F2),i in dom (Len F2) ) by A3, Def1, FINSEQ_1:3;
then A7: ( i + (Sum (Len F1)) in (Seg ((Sum (Len F1)) + (Sum (Len F2)))) \ (Seg (Sum (Len F1))) & min (Len F2),i >= 1 & min (Len F2),i <= len (Len F2) ) by A2, A3, A6, FINSEQ_3:27, XBOOLE_0:def 5;
then A8: ( min (Len (F1 ^ F2)),(i + (Sum (Len F1))) = (min (Len F2),((i + (Sum (Len F1))) -' (Sum (Len F1)))) + (len (Len F1)) & (i + (Sum (Len F1))) -' (Sum (Len F1)) = (i + (Sum (Len F1))) - (Sum (Len F1)) & ((min (Len F2),i) + (len (Len F1))) -' 1 = ((min (Len F2),i) -' 1) + (len (Len F1)) ) by A1, Th9, NAT_D:38;
then ( (Width F1) ^ ((Width F2) | (min (Len F2),i)) = (Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) & (Width F1) ^ ((Width F2) | ((min (Len F2),i) -' 1)) = (Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1) & (Len F1) ^ ((Len F2) | ((min (Len F2),i) -' 1)) = (Len (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1) ) by A3, A1, FINSEQ_6:16;
then A9: ( (Sum (Width F1)) + (Sum ((Width F2) | (min (Len F2),i))) = Sum ((Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),(i + (Sum (Len F1))))) & (Sum (Width F1)) + (Sum ((Width F2) | ((min (Len F2),i) -' 1))) = Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1)) & (Sum (Len F1)) + (Sum ((Len F2) | ((min (Len F2),i) -' 1))) = Sum ((Len (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1)) ) by RVSUM_1:105;
( i in NAT & j in NAT ) by ORDINAL1:def 13;
then A10: ( (i + (Sum (Len F1))) -' ((Sum (Len F1)) + (Sum ((Len F2) | ((min (Len F2),i) -' 1)))) = i -' (Sum ((Len F2) | ((min (Len F2),i) -' 1))) & (j + (Sum (Width F1))) -' ((Sum (Width F1)) + (Sum ((Width F2) | ((min (Len F2),i) -' 1)))) = j -' (Sum ((Width F2) | ((min (Len F2),i) -' 1))) ) by PRGCOR_1:1;

per cases ( j <= Sum ((Width F2) | ((min (Len F2),i) -' 1)) or j > Sum ((Width F2) | (min (Len F2),i)) or ( j > Sum ((Width F2) | ((min (Len F2),i) -' 1)) & j <= Sum ((Width F2) | (min (Len F2),i)) ) ) ;

suppose A11: ( j <= Sum ((Width F2) | ((min (Len F2),i) -' 1)) or j > Sum ((Width F2) | (min (Len F2),i)) ) ; :: thesis: (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))

then ( j + (Sum (Width F1)) <= Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1)) or j + (Sum (Width F1)) > Sum ((Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),(i + (Sum (Len F1))))) ) by A9, XREAL_1:9, XREAL_1:10;
then ( (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1))) = d & (block_diagonal F2,d) * i,j = d ) by A4, A5, A11, Def5;
hence (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1))) ; :: thesis: verum

end;

suppose A12: ( j > Sum ((Width F2) | ((min (Len F2),i) -' 1)) & j <= Sum ((Width F2) | (min (Len F2),i)) ) ; :: thesis: (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1)))

then ( j + (Sum (Width F1)) > Sum ((Width (F1 ^ F2)) | ((min (Len (F1 ^ F2)),(i + (Sum (Len F1)))) -' 1)) & j + (Sum (Width F1)) <= Sum ((Width (F1 ^ F2)) | (min (Len (F1 ^ F2)),(i + (Sum (Len F1))))) ) by A9, XREAL_1:9, XREAL_1:10;
then ( (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1))) = ((F1 ^ F2) . (min (Len (F1 ^ F2)),(i + (Sum (Len F1))))) * (i -' (Sum ((Len F2) | ((min (Len F2),i) -' 1)))),(j -' (Sum ((Width F2) | ((min (Len F2),i) -' 1)))) & (block_diagonal F2,d) * i,j = (F2 . (min (Len F2),i)) * (i -' (Sum ((Len F2) | ((min (Len F2),i) -' 1)))),(j -' (Sum ((Width F2) | ((min (Len F2),i) -' 1)))) ) by A4, A5, A9, A12, A10, Def5;
hence (block_diagonal F2,d) * i,j = (block_diagonal (F1 ^ F2),d) * (i + (Sum (Len F1))),(j + (Sum (Width F1))) by A8, A3, A7, FINSEQ_1:86; :: thesis: verum

end;

end;