theorem Th44: :: EUCLID_7:45

for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B = RN_Base n holds
B is Basis of RealVectSpace (Seg n)