let R be Ring; :: thesis: for P being Ideal of R
for M being Submodule of P
for a being BinOp of P
for z being Element of P
for m being Function of [:P, the carrier of R:],P st a = the addF of R | [:P,P:] & m = the multF of R | [:P, the carrier of R:] & z = the ZeroF of R holds
RightModStr(# the carrier of M, the addF of M, the ZeroF of M, the rmult of M #) = RightModStr(# P,a,z,m #)
let P be Ideal of R; :: thesis: for M being Submodule of P
for a being BinOp of P
for z being Element of P
for m being Function of [:P, the carrier of R:],P st a = the addF of R | [:P,P:] & m = the multF of R | [:P, the carrier of R:] & z = the ZeroF of R holds
RightModStr(# the carrier of M, the addF of M, the ZeroF of M, the rmult of M #) = RightModStr(# P,a,z,m #)
let M be Submodule of P; :: thesis: for a being BinOp of P
for z being Element of P
for m being Function of [:P, the carrier of R:],P st a = the addF of R | [:P,P:] & m = the multF of R | [:P, the carrier of R:] & z = the ZeroF of R holds
RightModStr(# the carrier of M, the addF of M, the ZeroF of M, the rmult of M #) = RightModStr(# P,a,z,m #)
A1: the carrier of M = P by Def15;
set V = RightModule R;
( 0. M = 0. (RightModule R) & the addF of M = the addF of (RightModule R) | [:P,P:] & the rmult of M = the rmult of (RightModule R) | [:P, the carrier of R:] ) by A1, RMOD_2:def 2;
hence for a being BinOp of P
for z being Element of P
for m being Function of [:P, the carrier of R:],P st a = the addF of R | [:P,P:] & m = the multF of R | [:P, the carrier of R:] & z = the ZeroF of R holds
RightModStr(# the carrier of M, the addF of M, the ZeroF of M, the rmult of M #) = RightModStr(# P,a,z,m #) by Def15; :: thesis: verum