theorem Th26: :: VECTSP_2:26
for R1, R2 being Ring holds BiModule (R1,R2) is BiMod of R1,R2