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