:: deftheorem Def6 defines BinOps PRVECT_1:def 6 :
for a being non-empty non empty Function
for b₂ being Function holds
( b₂ is BinOps of a iff ( dom b₂ = dom a & ( for i being Element of dom a holds b₂ . i is BinOp of (a . i) ) ) );