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