theorem :: ZMODUL01:47

for V being strict Z_Module
for W being strict Submodule of V st the carrier of W = the carrier of V holds
W = V by VECTSP_4:31;