theorem :: ZMODUL02:58

for V being Z_Module holds {} the carrier of V is linearly-independent ;