let G be Group; :: thesis: for H being Subgroup of G
for phi being Automorphism of G holds H,phi .: H are_isomorphic
let H be Subgroup of G; :: thesis: for phi being Automorphism of G holds H,phi .: H are_isomorphic
let phi be Automorphism of G; :: thesis: H,phi .: H are_isomorphic
H, Image (phi | H) are_isomorphic by Lm3, GROUP_6:68;
hence H,phi .: H are_isomorphic by GRSOLV_1:def 3; :: thesis: verum