theorem Th4: :: LPSPACE1:4

for V being non empty RLSStruct
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 by ZFMISC_1:87, FUNCT_1:49;