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