for R1, R2 being Ring holds BiModule (R1,R2) is BiMod of R1,R2