:: deftheorem Def2 defines [: PRVECT_2:def 2 :
for F being Domain-Sequence
for X being non empty set
for p being MultOps of X,F
for b₄ being Function of [:X,(product F):],(product F) holds
( b₄ = [:p:] iff for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b₄ . (x,d)) . i = (p . i) . (x,(d . i)) );