block_diagonal (S,d) is Matrix of Sum (Len S), Sum (Width S),D ;
hence block_diagonal (S,d) is Matrix of Sum (Len S),D by Th46; :: thesis: verum