let G be Group; :: thesis: for H being strict Subgroup of G holds
( H is characteristic Subgroup of G iff for phi being Automorphism of G holds Image (phi | H) is Subgroup of H )
let H be strict Subgroup of G; :: thesis: ( H is characteristic Subgroup of G iff for phi being Automorphism of G holds Image (phi | H) is Subgroup of H )
thus ( H is characteristic Subgroup of G implies for phi being Automorphism of G holds Image (phi | H) is Subgroup of H ) :: thesis: ( ( for phi being Automorphism of G holds Image (phi | H) is Subgroup of H ) implies H is characteristic Subgroup of G )

proof

assume B1: H is characteristic Subgroup of G ; :: thesis: for phi being Automorphism of G holds Image (phi | H) is Subgroup of H
let phi be Automorphism of G; :: thesis: Image (phi | H) is Subgroup of H
( Image (phi | H) = H & H is Subgroup of H ) by B1, GROUP_2:54, Def3;
hence Image (phi | H) is Subgroup of H ; :: thesis: verum

end;

thus ( ( for phi being Automorphism of G holds Image (phi | H) is Subgroup of H ) implies H is characteristic Subgroup of G ) :: thesis: verum

proof

assume A1: for phi being Automorphism of G holds Image (phi | H) is Subgroup of H ; :: thesis: H is characteristic Subgroup of G
A2: for phi being Automorphism of G holds H is Subgroup of Image (phi | H)

proof

let phi be Automorphism of G; :: thesis: H is Subgroup of Image (phi | H)
consider psi being Automorphism of G such that
B1: psi = phi " and
B2: Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) by A1, Th16;
consider psi2 being Automorphism of G such that
B3: psi2 = phi " and
B4: multMagma(# the carrier of H, the multF of H #) = Image (phi | (Image (psi2 | H))) by Th17;
thus H is Subgroup of Image (phi | H) by B1, B2, B3, B4; :: thesis: verum

end;

for phi being Automorphism of G holds H = Image (phi | H)

proof

let phi be Automorphism of G; :: thesis: H = Image (phi | H)
( H is Subgroup of Image (phi | H) & Image (phi | H) is Subgroup of H ) by A1, A2;
hence H = Image (phi | H) by GROUP_2:55; :: thesis: verum

end;

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

end;