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