for n being Nat
for B being Orthogonal_Basis of n holds card B = n