let G be Group; :: thesis: for phi being Automorphism of G
for H being Subgroup of G st ( for h being Element of H holds phi . h in H ) holds
Image (phi | H) is Subgroup of H
let phi be Automorphism of G; :: thesis: for H being Subgroup of G st ( for h being Element of H holds phi . h in H ) holds
Image (phi | H) is Subgroup of H
let H be Subgroup of G; :: thesis: ( ( for h being Element of H holds phi . h in H ) implies Image (phi | H) is Subgroup of H )
assume A1: for h being Element of H holds phi . h in H ; :: thesis: Image (phi | H) is Subgroup of H
for y being object st y in rng (phi | H) holds
y in the carrier of H

proof

let y be object ; :: thesis: ( y in rng (phi | H) implies y in the carrier of H )
assume y in rng (phi | H) ; :: thesis: y in the carrier of H
then consider x being object such that
B1: x in dom (phi | H) and
B2: y = (phi | H) . x by FUNCT_1:def 3;
B3: x in H by B1;
reconsider x = x as Element of H by B1;
( phi . x in H & x is Element of G ) by A1, GROUP_2:42;
hence y in the carrier of H by B2, B3, Th1; :: thesis: verum

end;

then rng (phi | H) c= the carrier of H ;
then the carrier of (Image (phi | H)) c= the carrier of H by GROUP_6:44;
hence Image (phi | H) is Subgroup of H by GROUP_2:57; :: thesis: verum