theorem Th49: :: EUCLID_7:50

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