let K, L be Ring; :: thesis: for V being non empty VectSpStr of K
for W being non empty RightModStr of L
for v1, v2 being Vector of
for w1, w2 being Vector of st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let V be non empty VectSpStr of K; :: thesis: for W being non empty RightModStr of L
for v1, v2 being Vector of
for w1, w2 being Vector of 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 U2 of (opp V) #) = addLoopStr(# the carrier of V,the addF of V,the U2 of V #) by Th9;
let W be non empty RightModStr of L; :: thesis: for v1, v2 being Vector of
for w1, w2 being Vector of st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let v1, v2 be Vector of ; :: thesis: for w1, w2 being Vector of st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let w1, w2 be Vector of ; :: 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