let V be Z_Module; :: thesis: for W being strict Submodule of V st ( for v being VECTOR of V holds v in W ) holds
W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
let W be strict Submodule of V; :: thesis: ( ( for v being VECTOR of V holds v in W ) implies W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) )
assume for v being VECTOR of V holds v in W ; :: thesis: W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
then for v being VECTOR of V holds
( v in W iff v in (Omega). V ) ;
hence W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Th46; :: thesis: verum