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. () & the addF of M = the addF of () | [:P,P:] & the rmult of M = the rmult of () | [:P, the carrier of R:] ) by ;
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