:: deftheorem YDef2 defines prod_MLT VECTSP12:def 6 :
for K being Ring
for G, F being non empty ModuleStr over K
for b₄ being Function of [: the carrier of K,[: 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 Element of K
for g being Vector of G
for f being Vector of F holds b₄ . (r,[g,f]) = [(r * g),(r * f)] );