let K, L be Ring; :: thesis: for V being non empty VectSpStr of K
for W being non empty RightModStr of L
for x being Scalar of
for y being Scalar of
for v being Vector of
for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let V be non empty VectSpStr of K; :: thesis: for W being non empty RightModStr of L
for x being Scalar of
for y being Scalar of
for v being Vector of
for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let W be non empty RightModStr of L; :: thesis: for x being Scalar of
for y being Scalar of
for v being Vector of
for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let x be Scalar of ; :: thesis: for y being Scalar of
for v being Vector of
for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let y be Scalar of ; :: thesis: for v being Vector of
for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let v be Vector of ; :: thesis: for w being Vector of st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let w be Vector of ; :: thesis: ( L = opp K & W = opp V & x = y & v = w implies w * y = x * v )
assume that
A1: ( L = opp K & W = opp V ) and
A2: ( x = y & v = w ) ; :: thesis: w * y = x * v
set o = the lmult of V;
opp the lmult of V = the rmult of (opp V) by Th10;
hence w * y = (opp the lmult of V) . w,y by A1, VECTSP_2:def 15
.= x * v by A2, Th1 ;
:: thesis: verum