theorem :: MOD_4:11

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