for r being Real
for n being Nat
for a, b being Element of F_Real st a = cos r & b = sin r holds
Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real