theorem Th2: :: CONVFUN1:2

for X, Y being non empty RLSStruct
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y
for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) st u1 = [x1,y1] & u2 = [x2,y2] holds
u1 + u2 = [(x1 + x2),(y1 + y2)] by Def1;