theorem Th60: :: MATRIXJ1:60

for i, j being Nat
for K being Field holds block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))