let K, L be Ring; 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; 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; 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; 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; ( W = opp V & v1 = w1 & v2 = w2 implies w1 + w2 = v1 + v2 )
assume
( W = opp V & v1 = w1 & v2 = w2 )
; w1 + w2 = v1 + v2
hence
w1 + w2 = v1 + v2
by A1; verum