set W = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #);
set V = Rat-Module ;
G1: ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is Z_Module by ZMODUL01:164;
P2: 0. ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) = 0. Rat-Module ;
the addF of Rat-Module || the carrier of ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) = the addF of ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) by LMLT12, GAUSSINT:13, NUMBERS:14, RELAT_1:74, ZFMISC_1:96;
hence ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is Submodule of Rat-Module by G1, P2, LMLT11, NUMBERS:14, VECTSP_4:def 2; :: thesis: verum