let G be non trivial Group; :: thesis: for H being Subgroup of G
for phi being Automorphism of G st H is proper Subgroup of G holds
Image (phi | H) is proper Subgroup of G
let H be Subgroup of G; :: thesis: for phi being Automorphism of G st H is proper Subgroup of G holds
Image (phi | H) is proper Subgroup of G
let phi be Automorphism of G; :: thesis: ( H is proper Subgroup of G implies Image (phi | H) is proper Subgroup of G )
set UH = the carrier of H;
set UG = the carrier of G;
A1: ( phi is one-to-one & phi is onto & the carrier of H is non empty Subset of the carrier of G & phi is Function of the carrier of G, the carrier of G ) by GROUP_2:def 5;
assume H is proper Subgroup of G ; :: thesis: Image (phi | H) is proper Subgroup of G
then not the carrier of G \ the carrier of H is empty by Th11;
then consider x being object such that
A2: x in the carrier of G \ the carrier of H by XBOOLE_0:def 1;
A3: ( x in G & not x in H ) by A2, XBOOLE_0:def 5;
A4: not phi . x in phi .: H

proof

not phi . x in phi .: the carrier of H by A1, A3, Th5;
hence not phi . x in phi .: H by GRSOLV_1:8; :: thesis: verum

end;

phi . x is Element of G

proof

( dom phi = the carrier of G & rng phi = the carrier of G ) by A1, FUNCT_2:def 1;
hence phi . x is Element of G by A2, FUNCT_1:def 3; :: thesis: verum

end;

then phi .: H is proper by A4;
hence Image (phi | H) is proper Subgroup of G by GRSOLV_1:def 3; :: thesis: verum