let K, L be Ring; :: thesis: for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for x being Scalar of K
for y being Scalar of L
for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let V be non empty ModuleStr over K; :: thesis: for W being non empty RightModStr over L
for x being Scalar of K
for y being Scalar of L
for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let W be non empty RightModStr over L; :: thesis: for x being Scalar of K
for y being Scalar of L
for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let x be Scalar of K; :: thesis: for y being Scalar of L
for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let y be Scalar of L; :: thesis: for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let v be Vector of V; :: thesis: for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let w be Vector of W; :: thesis: ( V = opp W & x = y & v = w implies w * y = x * v )
assume A1: ( V = opp W & x = y & v = w ) ; :: thesis: w * y = x * v
set o = the rmult of W;
A2: opp the rmult of W = the lmult of (opp W) by Th10;
thus w * y = the rmult of W . (w,y) by VECTSP_2:def 7
.= x * v by A1, A2, FUNCT_4:def 8 ; :: thesis: verum