:: deftheorem defines BiModule VECTSP_2:def 7 :
for R1, R2 being Ring holds BiModule (R1,R2) = BiModStr(# {0},op2,op0,(pr2 ( the carrier of R1,{0})),(pr1 ({0}, the carrier of R2)) #);