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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & x = y & v = w holds

w * y = x * v

let v be Vector of V; :: thesis: for w being Vector of W st L = opp K & W = opp V & x = y & v = w holds

w * y = x * v

let w be Vector of W; :: 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 Th8;

hence w * y = (opp the lmult of V) . (w,y) by A1, VECTSP_2:def 7

.= x * v by A2, FUNCT_4:def 8 ;

:: thesis: verum

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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & 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 L = opp K & W = opp V & x = y & v = w holds

w * y = x * v

let v be Vector of V; :: thesis: for w being Vector of W st L = opp K & W = opp V & x = y & v = w holds

w * y = x * v

let w be Vector of W; :: 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 Th8;

hence w * y = (opp the lmult of V) . (w,y) by A1, VECTSP_2:def 7

.= x * v by A2, FUNCT_4:def 8 ;

:: thesis: verum