let G be finite Group; :: thesis: for N being strict normal Subgroup of G st card N, index N are_coprime holds
N is characteristic Subgroup of G
let N be strict normal Subgroup of G; :: thesis: ( card N, index N are_coprime implies N is characteristic Subgroup of G )
assume A1: card N, index N are_coprime ; :: thesis: N is characteristic Subgroup of G
consider m being Nat such that
A2: m = card N ;
consider n being Nat such that
A3: n = index N ;
A4: card G = m * n by A2, A3, GROUP_2:147;
for phi being Automorphism of G holds Image (phi | N) = N

proof

let phi be Automorphism of G; :: thesis: Image (phi | N) = N
set K = Image (phi | N);
reconsider K = Image (phi | N) as strict normal Subgroup of G by Th49;
K = phi .: N by GRSOLV_1:def 3;
then B1: card K = card N by Th19, GROUP_6:73;
set d = card (N /\ K);
card (N /\ K) divides m

proof

N /\ K is Subgroup of N by GROUP_2:88;
hence card (N /\ K) divides m by A2, GROUP_2:148; :: thesis: verum

end;

then consider q being Nat such that
B2: m = (card (N /\ K)) * q by NAT_D:def 3;
B3: q <> 0 by A2, B2;
card (N "\/" K) = m * q

proof

K /\ N = N /\ K

proof

carr (K /\ N) = (carr K) /\ (carr N) by GROUP_2:def 10
.= carr (N /\ K) by GROUP_2:def 10 ;
hence K /\ N = N /\ K by GROUP_2:59; :: thesis: verum

end;

then (card (N /\ K)) * (card (N "\/" K)) = m * ((card (N /\ K)) * q) by A2, B1, B2, Th70
.= (card (N /\ K)) * (m * q) ;
hence card (N "\/" K) = m * q by XCMPLX_1:5; :: thesis: verum

end;

then q divides n by A2, A4, Th67a, GROUP_2:148;
then q = 1 by A1, A2, A3, B2, B3, Th68;
hence Image (phi | N) = N by A2, B1, B2, Th66; :: thesis: verum

end;

hence N is characteristic Subgroup of G by Def3; :: thesis: verum