:: deftheorem Def3 defines incl2 GROUP_24:def 3 :
for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for b₄ being Function of A,(semidirect_product (G,A,phi)) holds
( b₄ = incl2 (G,A,phi) iff for a being Element of A holds b₄ . a = <*(1_ G),a*> );