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_0:51; :: thesis: verum