:: deftheorem Def7 defines Funcs FUNCT_6:def 8 :
for f being Function
for X being set
for b₃ being Function holds
( b₃ = Funcs (f,X) iff ( dom b₃ = dom f & ( for x being object st x in dom f holds
b₃ . x = Funcs ((f . x),X) ) ) );