:: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def 2 :
for X, Y being non empty RLSStruct
for b₃ being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds
( b₃ = Mult_in_Prod_of_RLS (X,Y) iff for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b₃ . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] );