let G be Group; :: thesis: for H being Subgroup of G
for phi being Automorphism of G st ( for f being Automorphism of G holds Image (f | H) is Subgroup of H ) holds
ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )
let H be Subgroup of G; :: thesis: for phi being Automorphism of G st ( for f being Automorphism of G holds Image (f | H) is Subgroup of H ) holds
ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )
let phi be Automorphism of G; :: thesis: ( ( for f being Automorphism of G holds Image (f | H) is Subgroup of H ) implies ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) ) )
assume A1: for f being Automorphism of G holds Image (f | H) is Subgroup of H ; :: thesis: ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
take psi ; :: thesis: ( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )
thus psi = phi " ; :: thesis: Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H)
Image (psi | H) is Subgroup of H by A1;
then phi .: (Image (psi | H)) is Subgroup of phi .: H by GRSOLV_1:12;
then Image (phi | (Image (psi | H))) is Subgroup of phi .: H by GRSOLV_1:def 3;
hence Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) by GRSOLV_1:def 3; :: thesis: verum