let R1, R2 be Ring; :: thesis: BiModule (R1,R2) is BiMod of R1,R2
for x, y being Scalar of R1
for p, q being Scalar of R2
for v, w being Vector of (BiModule (R1,R2)) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ R1) * v = v & (v + w) * p = (v * p) + (w * p) & v * (p + q) = (v * p) + (v * q) & v * (q * p) = (v * q) * p & v * (1_ R2) = v & x * (v * p) = (x * v) * p ) by Lm9;
hence BiModule (R1,R2) is BiMod of R1,R2 by Def8, Def9, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; :: thesis: verum