let V be non empty RLSStruct ; :: thesis: for V1 being non empty add-closed multi-closed Subset of V
for v, u being VECTOR of V
for w1, w2 being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w1 = v & w2 = u holds
w1 + w2 = v + u
let V1 be non empty add-closed multi-closed Subset of V; :: thesis: for v, u being VECTOR of V
for w1, w2 being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w1 = v & w2 = u holds
w1 + w2 = v + u
let v, u be VECTOR of V; :: thesis: for w1, w2 being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w1 = v & w2 = u holds
w1 + w2 = v + u
let w1, w2 be VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #); :: thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u )
assume A1: ( w1 = v & w2 = u ) ; :: thesis: w1 + w2 = v + u
then [v,u] in [:V1,V1:] by ZFMISC_1:106;
hence w1 + w2 = v + u by A1, FUNCT_1:72; :: thesis: verum