:: deftheorem Def8 defines [: PRVECT_1:def 8 :
for a being Domain-Sequence
for b being BinOps of a
for b₃ being BinOp of (product a) holds
( b₃ = [:b:] iff for f, g being Element of product a
for i being Element of dom a holds (b₃ . (f,g)) . i = (b . i) . ((f . i),(g . i)) );