let V be Z_Module; :: thesis: for W being Submodule of V holds ((Omega). V) + W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
let W be Submodule of V; :: thesis: ((Omega). V) + W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
the carrier of W c= the carrier of V by Def9;
hence ((Omega). V) + W = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm7; :: thesis: verum