( len (block_diagonal F,d) = Sum (Len F) & width (block_diagonal F,d) = Sum (Width F) ) by Def5;
hence block_diagonal F,d is Matrix of Sum (Len F), Sum (Width F),D by MATRIX_2:7; :: thesis: verum