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