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 (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
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 (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
let d be Element of D; :: thesis: for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
let F1, F2 be FinSequence_of_Matrix of D; :: thesis: ( [i,j] in Indices (block_diagonal (F1,d)) implies (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j) )
set B1 = block_diagonal (F1,d);
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 B12 = block_diagonal ((F1 ^ F2),d);
A1: len F1 = len (Width F1) by CARD_1:def 7;
A2: len (block_diagonal (F1,d)) = Sum (Len F1) by Def5;
assume A3: [i,j] in Indices (block_diagonal (F1,d)) ; :: thesis: (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
then i in dom (block_diagonal (F1,d)) by ZFMISC_1:87;
then A4: i in Seg (len (block_diagonal (F1,d))) by FINSEQ_1:def 3;
then A5: min ((Len F1),i) in dom (Len F1) by A2, Def1;
then A6: min ((Len F1),i) <= len (Len F1) by FINSEQ_3:25;
(Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
then A7: min ((Len F1),i) = min ((Len (F1 ^ F2)),i) by A4, A2, Th8;
A8: dom (Len F1) = dom F1 by Def3;
A9: (Width F1) ^ (Width F2) = Width (F1 ^ F2) by Th18;
A10: (Len F1) ^ (Len F2) = Len (F1 ^ F2) by Th14;
A11: Indices (block_diagonal (F1,d)) is Subset of (Indices (block_diagonal ((F1 ^ F2),d))) by Th25;
A12: len (Len F1) = len F1 by CARD_1:def 7;
then A13: ((Width F1) ^ (Width F2)) | (min ((Len (F1 ^ F2)),i)) = (Width F1) | (min ((Len F1),i)) by A7, A6, A1, FINSEQ_5:22;
A14: (min ((Len F1),i)) -' 1 <= min ((Len F1),i) by NAT_D:35;
then A15: ((Len F1) ^ (Len F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1) = (Len F1) | ((min ((Len F1),i)) -' 1) by A7, A6, FINSEQ_5:22, XXREAL_0:2;
A16: ((Width F1) ^ (Width F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1) = (Width F1) | ((min ((Len F1),i)) -' 1) by A7, A6, A14, A12, A1, FINSEQ_5:22, XXREAL_0:2;

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

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

then (block_diagonal (F1,d)) * (i,j) = d by A3, Def5;
hence (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j) by A3, A11, A13, A16, A9, A17, Def5; :: thesis: verum

end;

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

then A19: (block_diagonal (F1,d)) * (i,j) = (F1 . (min ((Len F1),i))) * ((i -' (Sum ((Len F1) | ((min ((Len F1),i)) -' 1)))),(j -' (Sum ((Width F1) | ((min ((Len F1),i)) -' 1))))) by A3, Def5;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = ((F1 ^ F2) . (min ((Len F1),i))) * ((i -' (Sum ((Len F1) | ((min ((Len F1),i)) -' 1)))),(j -' (Sum ((Width F1) | ((min ((Len F1),i)) -' 1))))) by A3, A11, A7, A13, A16, A15, A9, A10, A18, Def5;
hence (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j) by A5, A8, A19, FINSEQ_1:def 7; :: thesis: verum

end;

end;