theorem :: ZMODUL02:43

for V being Z_Module holds the carrier of (LC_Z_Module V) = LinComb V ;