:: deftheorem Def1 defines prod_ADD PRVECT_3:def 1 :
for G, F being non empty addLoopStr
for b₃ being BinOp of [: the carrier of G, the carrier of F:] holds
( b₃ = prod_ADD (G,F) iff for g1, g2 being Point of G
for f1, f2 being Point of F holds b₃ . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] );