:: deftheorem Def9 defines " FUNCT_2:def 9 :
for T, S being non empty set
for f being Function of T,S
for G being Subset-Family of S
for b₅ being Subset-Family of T holds
( b₅ = f " G iff for A being Subset of T holds
( A in b₅ iff ex B being Subset of S st
( B in G & A = f " B ) ) );