for K being Field
for f being FinSequence of NAT holds block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f))