let K, L be Ring; :: thesis: for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for v1, v2 being Vector of V
for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let V be non empty ModuleStr over K; :: thesis: for W being non empty RightModStr over L
for v1, v2 being Vector of V
for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
A1: addLoopStr(# the carrier of (opp V), the addF of (opp V), the ZeroF of (opp V) #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) by Th7;
let W be non empty RightModStr over L; :: thesis: for v1, v2 being Vector of V
for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let v1, v2 be Vector of V; :: thesis: for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let w1, w2 be Vector of W; :: thesis: ( W = opp V & v1 = w1 & v2 = w2 implies w1 + w2 = v1 + v2 )
assume ( W = opp V & v1 = w1 & v2 = w2 ) ; :: thesis: w1 + w2 = v1 + v2
hence w1 + w2 = v1 + v2 by A1; :: thesis: verum