let G be Group; :: thesis: for H being Subgroup of G holds
( H is characteristic iff for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H c= the carrier of H )
let H be Subgroup of G; :: thesis: ( H is characteristic iff for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H c= the carrier of H )
thus ( H is characteristic implies for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H c= the carrier of H ) by ThAlt1; :: thesis: ( ( for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H c= the carrier of H ) implies H is characteristic )
assume A3: for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H c= the carrier of H ; :: thesis: H is characteristic
for phi being Automorphism of G holds Image (phi | H) is Subgroup of H

proof

let phi be Automorphism of G; :: thesis: Image (phi | H) is Subgroup of H
phi .: the carrier of H = (phi | the carrier of H) .: the carrier of H by FUNCT_2:97
.= (phi | H) .: the carrier of H by GRSOLV_1:def 2
.= the carrier of (Image (phi | H)) by GROUP_6:def 10 ;
hence Image (phi | H) is Subgroup of H by A3, GROUP_2:57; :: thesis: verum

end;

hence H is characteristic by Th40; :: thesis: verum