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