:: deftheorem Def19 defines ** PBOOLE:def 19 :
for F, G being Function-yielding Function
for b₃ being Function holds
( b₃ = G ** F iff ( dom b₃ = (dom F) /\ (dom G) & ( for i being object st i in dom b₃ holds
b₃ . i = (G . i) * (F . i) ) ) );