:: deftheorem Def3 defines FuncLatt LATSUBGR:def 3 :
for G1, G2 being Group
for f being Function of the carrier of G1, the carrier of G2
for b₄ being Function of the carrier of (lattice G1), the carrier of (lattice G2) holds
( b₄ = FuncLatt f iff for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
b₄ . H = gr A );