for X being RealLinearSpace holds {(0. X)} is circled by Th13;