:: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def 1 :
for X, Y being non empty RLSStruct
for b₃ being BinOp of [: the carrier of X, the carrier of Y:] holds
( b₃ = Add_in_Prod_of_RLS (X,Y) iff for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b₃ . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] );