:: deftheorem Def5 defines block_diagonal MATRIXJ1:def 5 :
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D
for b₄ being Matrix of D holds
( b₄ = block_diagonal (F,d) iff ( len b₄ = Sum (Len F) & width b₄ = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b₄ holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b₄ * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b₄ * (i,j) = (F . (min ((Len F),i))) * ((i -' (Sum ((Len F) | ((min ((Len F),i)) -' 1)))),(j -' (Sum ((Width F) | ((min ((Len F),i)) -' 1))))) ) ) ) ) );