:: deftheorem Def2 defines prod_MLT PRVECT_3:def 2 :
for G, F being non empty RLSStruct
for b₃ being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b₃ = prod_MLT (G,F) iff for r being Real
for g being Point of G
for f being Point of F holds b₃ . (r,[g,f]) = [(r * g),(r * f)] );