let L, E be Z_Module; :: thesis: ( ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) implies L is Submodule of E )
assume AS: ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) ; :: thesis: L is Submodule of E
P2: 0. L = 0. E by AS;
P3: the addF of L = the addF of E || the carrier of L by AS;
the lmult of L = the lmult of E | [: the carrier of INT.Ring, the carrier of L:] by AS;
hence L is Submodule of E by AS, P2, P3, VECTSP_4:def 2; :: thesis: verum