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 = 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 = the carrier of H )

hereby :: thesis: ( ( for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H = the carrier of H ) implies H is characteristic )

assume A1: H is characteristic ; :: thesis: for phi being Homomorphism of G,G st phi is bijective holds
the carrier of H = phi .: the carrier of H
let phi be Homomorphism of G,G; :: thesis: ( phi is bijective implies the carrier of H = phi .: the carrier of H )
assume phi is bijective ; :: thesis: the carrier of H = phi .: the carrier of H
then phi is Automorphism of G ;
then the carrier of (Image (phi | H)) = the carrier of H by A1;
then (phi | H) .: the carrier of H = the carrier of H by GROUP_6:def 10;
hence the carrier of H = (phi | the carrier of H) .: the carrier of H by GRSOLV_1:def 2
.= phi .: the carrier of H by FUNCT_2:97 ;
:: thesis: verum

end;

assume A3: for phi being Homomorphism of G,G st phi is bijective holds
phi .: the carrier of H = the carrier of H ; :: thesis: H is characteristic
for phi being Automorphism of G holds Image (phi | H) = multMagma(# the carrier of H, the multF of H #)

proof

let phi be Automorphism of G; :: thesis: Image (phi | H) = multMagma(# the carrier of H, the multF of H #)
the carrier of H = phi .: the carrier of H by A3
.= (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) = multMagma(# the carrier of H, the multF of H #) by GROUP_2:59; :: thesis: verum

end;

hence H is characteristic ; :: thesis: verum