let G be Group; :: thesis: for phi being Automorphism of G
for H being strict Subgroup of G
for K being Subgroup of G st Image (phi | H) is Subgroup of K holds
ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) )
let phi be Automorphism of G; :: thesis: for H being strict Subgroup of G
for K being Subgroup of G st Image (phi | H) is Subgroup of K holds
ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) )
let H be strict Subgroup of G; :: thesis: for K being Subgroup of G st Image (phi | H) is Subgroup of K holds
ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) )
let K be Subgroup of G; :: thesis: ( Image (phi | H) is Subgroup of K implies ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) ) )
assume A1: Image (phi | H) is Subgroup of K ; :: thesis: ex psi being Automorphism of G st
( psi = phi " & H is Subgroup of Image (psi | K) )
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
take psi ; :: thesis: ( psi = phi " & H is Subgroup of Image (psi | K) )
thus psi = phi " ; :: thesis: H is Subgroup of Image (psi | K)
consider phi0 being Automorphism of G such that
A2: phi0 = psi " and
A3: Image (psi | (Image (phi0 | H))) = multMagma(# the carrier of H, the multF of H #) by Th17;
A4: phi = phi0 by A2, FUNCT_1:43;
psi .: (Image (phi | H)) is Subgroup of psi .: K by A1, GRSOLV_1:12;
then Image (psi | (Image (phi | H))) is Subgroup of psi .: K by GRSOLV_1:def 3;
hence H is Subgroup of Image (psi | K) by A3, A4, GRSOLV_1:def 3; :: thesis: verum