:: deftheorem Def6 defines prod_NORM PRVECT_3:def 6 :
for G, F being non empty NORMSTR
for b₃ being Function of [: the carrier of G, the carrier of F:],REAL holds
( b₃ = prod_NORM (G,F) iff for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b₃ . (g,f) = |.v.| ) );