for n being Nat
for D being Orthogonal_Basis of n holds D is Basis of RealVectSpace (Seg n)