theorem :: RLVECT_3:16

for V being RealLinearSpace holds Lin ({} the carrier of V) = (0). V