take BiModule R1,R2 ; :: thesis: ( BiModule R1,R2 is Abelian & BiModule R1,R2 is add-associative & BiModule R1,R2 is right_zeroed & BiModule R1,R2 is right_complementable & BiModule R1,R2 is RightMod-like & BiModule R1,R2 is vector-distributive & BiModule R1,R2 is scalar-distributive & BiModule R1,R2 is scalar-associative & BiModule R1,R2 is scalar-unital & BiModule R1,R2 is BiMod-like & BiModule R1,R2 is strict )
thus ( BiModule R1,R2 is Abelian & BiModule R1,R2 is add-associative & BiModule R1,R2 is right_zeroed & BiModule R1,R2 is right_complementable ) ; :: thesis: ( BiModule R1,R2 is RightMod-like & BiModule R1,R2 is vector-distributive & BiModule R1,R2 is scalar-distributive & BiModule R1,R2 is scalar-associative & BiModule R1,R2 is scalar-unital & BiModule R1,R2 is BiMod-like & BiModule R1,R2 is strict )
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 RightMod-like & BiModule R1,R2 is vector-distributive & BiModule R1,R2 is scalar-distributive & BiModule R1,R2 is scalar-associative & BiModule R1,R2 is scalar-unital & BiModule R1,R2 is BiMod-like & BiModule R1,R2 is strict ) by Def23, Def24, VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29; :: thesis: verum