let i, j be Nat; :: thesis: for D being non empty set
for d being Element of D
for F1, F2 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 F1, F2 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 F1, F2 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 F1, F2 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: dom (block_diagonal ((F1 ^ F2),d)) = Seg (len (block_diagonal ((F1 ^ F2),d))) by FINSEQ_1:def 3;
A2: len (block_diagonal ((F1 ^ F2),d)) = Sum (Len (F1 ^ F2)) by Def5;
A3: (Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
then A4: Sum (Len (F1 ^ F2)) = (Sum (Len F1)) + (Sum (Len F2)) by RVSUM_1:75;
assume A5: [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 i > 0 by Th27;
then i + (Sum (Len F1)) > 0 + (Sum (Len F1)) by XREAL_1:6;
then A6: not i + (Sum (Len F1)) in Seg (Sum (Len F1)) by FINSEQ_1:1;
A7: [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d)) by A5, Th27;
then i + (Sum (Len F1)) in dom (block_diagonal ((F1 ^ F2),d)) by ZFMISC_1:87;
then A8: i + (Sum (Len F1)) in (Seg ((Sum (Len F1)) + (Sum (Len F2)))) \ (Seg (Sum (Len F1))) by A4, A1, A2, A6, XBOOLE_0:def 5;
then A9: min ((Len (F1 ^ F2)),(i + (Sum (Len F1)))) = (min ((Len F2),((i + (Sum (Len F1))) -' (Sum (Len F1))))) + (len (Len F1)) by A3, Th9;
A10: len (block_diagonal (F2,d)) = Sum (Len F2) by Def5;
A11: len (Width F1) = len F1 by CARD_1:def 7;
i in dom (block_diagonal (F2,d)) by A5, ZFMISC_1:87;
then i in Seg (len (block_diagonal (F2,d))) by FINSEQ_1:def 3;
then A12: min ((Len F2),i) in dom (Len F2) by A10, Def1;
then A13: min ((Len F2),i) <= len (Len F2) by FINSEQ_3:25;
A14: (i + (Sum (Len F1))) -' (Sum (Len F1)) = (i + (Sum (Len F1))) - (Sum (Len F1)) by A8, Th9;
A15: (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;
A16: len (Len F2) = len F2 by CARD_1:def 7;
A17: (i + (Sum (Len F1))) -' ((Sum (Len F1)) + (Sum ((Len F2) | ((min ((Len F2),i)) -' 1)))) = i -' (Sum ((Len F2) | ((min ((Len F2),i)) -' 1))) by PRGCOR_1:1;
A18: len F1 = len (Len F1) by CARD_1:def 7;
A19: (Width F1) ^ (Width F2) = Width (F1 ^ F2) by Th18;
then (Width F1) ^ ((Width F2) | (min ((Len F2),i))) = (Width (F1 ^ F2)) | (min ((Len (F1 ^ F2)),(i + (Sum (Len F1))))) by A11, A18, A9, A14, FINSEQ_6:14;
then A20: (Sum (Width F1)) + (Sum ((Width F2) | (min ((Len F2),i)))) = Sum ((Width (F1 ^ F2)) | (min ((Len (F1 ^ F2)),(i + (Sum (Len F1)))))) by RVSUM_1:75;
A21: min ((Len F2),i) >= 1 by A12, FINSEQ_3:25;
then A22: ((min ((Len F2),i)) + (len (Len F1))) -' 1 = ((min ((Len F2),i)) -' 1) + (len (Len F1)) by NAT_D:38;
then (Len F1) ^ ((Len F2) | ((min ((Len F2),i)) -' 1)) = (Len (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),(i + (Sum (Len F1))))) -' 1) by A3, A9, A14, FINSEQ_6:14;
then A23: (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:75;
(Width F1) ^ ((Width F2) | ((min ((Len F2),i)) -' 1)) = (Width (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),(i + (Sum (Len F1))))) -' 1) by A19, A11, A18, A9, A14, A22, FINSEQ_6:14;
then A24: (Sum (Width F1)) + (Sum ((Width F2) | ((min ((Len F2),i)) -' 1))) = Sum ((Width (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),(i + (Sum (Len F1))))) -' 1)) by RVSUM_1:75;

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 A25: ( 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 A20, A24, XREAL_1:7, XREAL_1:8;
then (block_diagonal ((F1 ^ F2),d)) * ((i + (Sum (Len F1))),(j + (Sum (Width F1)))) = d by A7, Def5;
hence (block_diagonal (F2,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * ((i + (Sum (Len F1))),(j + (Sum (Width F1)))) by A5, A25, Def5; :: thesis: verum

end;

suppose A26: ( 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 A27: j + (Sum (Width F1)) <= Sum ((Width (F1 ^ F2)) | (min ((Len (F1 ^ F2)),(i + (Sum (Len F1)))))) by A20, XREAL_1:7;
A28: (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 A5, A26, Def5;
j + (Sum (Width F1)) > Sum ((Width (F1 ^ F2)) | ((min ((Len (F1 ^ F2)),(i + (Sum (Len F1))))) -' 1)) by A24, A26, XREAL_1:8;
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))))) by A7, A24, A23, A17, A15, A27, Def5;
hence (block_diagonal (F2,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * ((i + (Sum (Len F1))),(j + (Sum (Width F1)))) by A18, A16, A21, A13, A9, A14, A28, FINSEQ_1:65; :: thesis: verum

end;

end;