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), by Th46; :: thesis: verum