let G be Group; :: thesis: for H being Subgroup of G
for f being Automorphism of G st Image (f | H) = multMagma(# the carrier of H, the multF of H #) holds
f | H is Automorphism of H
let H be Subgroup of G; :: thesis: for f being Automorphism of G st Image (f | H) = multMagma(# the carrier of H, the multF of H #) holds
f | H is Automorphism of H
let f be Automorphism of G; :: thesis: ( Image (f | H) = multMagma(# the carrier of H, the multF of H #) implies f | H is Automorphism of H )
assume A1: Image (f | H) = multMagma(# the carrier of H, the multF of H #) ; :: thesis: f | H is Automorphism of H
set UH = the carrier of H;
reconsider fH = f | H as Function of the carrier of H, the carrier of H by A1, GROUP_6:49;
A2: fH is bijective

proof

thus fH is one-to-one by Lm3; :: according to FUNCT_2:def 4 :: thesis: fH is onto
the carrier of H = rng (f | H) by A1, GROUP_6:44
.= rng fH ;
hence fH is onto ; :: thesis: verum

end;

for x, y being Element of H holds fH . (x * y) = (fH . x) * (fH . y)

proof

let x, y be Element of H; :: thesis: fH . (x * y) = (fH . x) * (fH . y)
fH . (x * y) = ((f | H) . x) * ((f | H) . y) by GROUP_6:def 6
.= (fH . x) * (fH . y) by GROUP_2:43 ;
hence fH . (x * y) = (fH . x) * (fH . y) ; :: thesis: verum

end;

hence f | H is Automorphism of H by A2, GROUP_6:def 6; :: thesis: verum