consider H1 being strict Subgroup of G such that
A1: the carrier of H1 = ((a ") * H) * ((a ") ") by GROUP_2:127;
the carrier of H1 = ((a ") * (carr H)) * a by A1
.= (carr H) |^ a by Th50 ;
hence ex b₁ being strict Subgroup of G st the carrier of b₁ = (carr H) |^ a ; :: thesis: verum