for X, Y being non empty RLSStruct
for x being VECTOR of X
for y being VECTOR of Y
for u being VECTOR of (Prod_of_RLS (X,Y))
for p being Real st u = [x,y] holds
p * u = [(p * x),(p * y)] by Def2;