theorem :: ZMODUL02:67

for V being Z_Module holds Lin ({} the carrier of V) = (0). V by MOD_3:6;