set C = the carrier of S;
R is Subring of S by Def1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
then [: the carrier of R, the carrier of S:] c= [: the carrier of S, the carrier of S:] by ZFMISC_1:96;
then reconsider lm = the multF of S | [: the carrier of R, the carrier of S:] as Function of [: the carrier of R, the carrier of S:], the carrier of S by FUNCT_2:32;
take ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) ; :: thesis: ( the carrier of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the carrier of S & the addF of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the addF of S & the ZeroF of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = 0. S & the lmult of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the multF of S | [: the carrier of R, the carrier of S:] )
thus ( the carrier of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the carrier of S & the addF of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the addF of S & the ZeroF of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = 0. S & the lmult of ModuleStr(# the carrier of S, the addF of S,(0. S),lm #) = the multF of S | [: the carrier of R, the carrier of S:] ) ; :: thesis: verum