theorem :: MOD_4:14

for K being non empty doubleLoopStr
for W being non empty RightModStr over K
for o being Function of [: the carrier of W, the carrier of K:], the carrier of W
for x being Scalar of K
for y being Scalar of (opp K)
for v being Vector of W
for w being Vector of (opp W) st x = y & v = w holds
(opp o) . (y,w) = o . (v,x) by FUNCT_4:def 8;