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

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