let G be Group; :: thesis: for H being Subgroup of G
for phi being Automorphism of G holds
( phi | H is Homomorphism of H,(Image (phi | H)) & phi | H is one-to-one )
let H be Subgroup of G; :: thesis: for phi being Automorphism of G holds
( phi | H is Homomorphism of H,(Image (phi | H)) & phi | H is one-to-one )
let phi be Automorphism of G; :: thesis: ( phi | H is Homomorphism of H,(Image (phi | H)) & phi | H is one-to-one )
thus phi | H is Homomorphism of H,(Image (phi | H)) by GROUP_6:49; :: thesis: phi | H is one-to-one
Ker phi = (1). G by GROUP_6:56;
then Ker (phi | H) is Subgroup of (1). G by Th15;
then Ker (phi | H) = (1). G by Lm2
.= (1). H by GROUP_2:63 ;
hence phi | H is one-to-one by GROUP_6:56; :: thesis: verum