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