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