the carrier of (semidirect_product (G,A,phi)) = product (Carrier <*G,A*>) by Def1;
hence semidirect_product (G,A,phi) is constituted-Functions by MONOID_0:80; :: thesis: verum