:: deftheorem Def17 defines .. PRALG_1:def 19 :
for F being Function-yielding Function
for f, b₃ being Function holds
( b₃ = F .. f iff ( dom b₃ = (dom F) /\ (dom f) & ( for x being set st x in dom b₃ holds
b₃ . x = (F . x) . (f . x) ) ) );