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 V = opp W & 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 V = opp W & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let W be non empty RightModStr over L; :: thesis: for v1, v2 being Vector of V
for w1, w2 being Vector of W st V = opp W & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
A1: addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) by Th9;
let v1, v2 be Vector of V; :: thesis: for w1, w2 being Vector of W st V = opp W & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let w1, w2 be Vector of W; :: thesis: ( V = opp W & v1 = w1 & v2 = w2 implies w1 + w2 = v1 + v2 )
assume ( V = opp W & v1 = w1 & v2 = w2 ) ; :: thesis: w1 + w2 = v1 + v2
hence w1 + w2 = v1 + v2 by A1; :: thesis: verum