let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) st G is strict & G is trivial holds
semidirect_product (G,A,phi),A are_isomorphic
let phi be Homomorphism of A,(AutGroup G); :: thesis: ( G is strict & G is trivial implies semidirect_product (G,A,phi),A are_isomorphic )
assume A1: ( G is strict & G is trivial ) ; :: thesis: semidirect_product (G,A,phi),A are_isomorphic
then AutGroup G is trivial by Th70;
then phi = 1: (A,(AutGroup G)) by Th68;
then semidirect_product (G,A,phi) = product <*G,A*> by Th38;
hence semidirect_product (G,A,phi),A are_isomorphic by A1, Th72; :: thesis: verum