theorem Th47: :: EUCLID_7:48

{} is Basis of RealVectSpace (Seg 0)