theorem :: GROUP_22:66
for G being finite Group
for N being strict normal Subgroup of G st card N, index N are_coprime holds
N is characteristic Subgroup of G