theorem Th47: :: EUCLID_7:48
{} is Basis of RealVectSpace (Seg 0)