let G be Group; :: thesis: for H being Subgroup of G
for phi being Automorphism of G ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )
let H be Subgroup of G; :: thesis: for phi being Automorphism of G ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )
let phi be Automorphism of G; :: thesis: ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
take psi ; :: thesis: ( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )
thus psi = phi " ; :: thesis: Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #)
for g being Element of G holds
( g in Image (phi | (Image (psi | H))) iff g in H )

proof

let g be Element of G; :: thesis: ( g in Image (phi | (Image (psi | H))) iff g in H )
thus ( g in Image (phi | (Image (psi | H))) implies g in H ) :: thesis: ( g in H implies g in Image (phi | (Image (psi | H))) )

proof

assume g in Image (phi | (Image (psi | H))) ; :: thesis: g in H
then consider a being Element of (Image (psi | H)) such that
B1: g = (phi | (Image (psi | H))) . a by GROUP_6:45;
M1: ( a in Image (psi | H) & a is Element of G ) by GROUP_2:42;
then B2: phi . a = g by B1, Th1;
consider b being Element of H such that
B3: a = (psi | H) . b by M1, GROUP_6:45;
M2: ( b in H & b is Element of G ) by GROUP_2:42;
then b = phi . (psi . b) by Th4
.= g by M2, B2, B3, Th1 ;
hence g in H ; :: thesis: verum

end;

thus ( g in H implies g in Image (phi | (Image (psi | H))) ) :: thesis: verum

proof

assume B1: g in H ; :: thesis: g in Image (phi | (Image (psi | H)))
set a = (psi | H) . g;
B2: (psi | H) . g in Image (psi | H)

proof

g in dom (psi | H) by B1, FUNCT_2:def 1;
then (psi | H) . g in (psi | H) .: the carrier of H by FUNCT_1:def 6;
hence (psi | H) . g in Image (psi | H) by GROUP_6:def 10; :: thesis: verum

end;

set K = Image (psi | H);
set b = (phi | (Image (psi | H))) . ((psi | H) . g);
B3: (phi | (Image (psi | H))) . ((psi | H) . g) in Image (phi | (Image (psi | H)))

proof

(psi | H) . g in dom (phi | (Image (psi | H))) by B2, FUNCT_2:def 1;
then (phi | (Image (psi | H))) . ((psi | H) . g) in (phi | (Image (psi | H))) .: the carrier of (Image (psi | H)) by FUNCT_1:def 6;
hence (phi | (Image (psi | H))) . ((psi | H) . g) in Image (phi | (Image (psi | H))) by GROUP_6:def 10; :: thesis: verum

end;

thus g in Image (phi | (Image (psi | H))) :: thesis: verum

proof

B4: psi . g = (psi | H) . g by B1, Th1;
(psi | H) . g is Element of G by B2, GROUP_2:42;
then (phi | (Image (psi | H))) . ((psi | H) . g) = phi . ((psi | H) . g) by B2, Th1
.= g by B4, Th4 ;
hence g in Image (phi | (Image (psi | H))) by B3; :: thesis: verum

end;

end;

end;

hence Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) by GROUP_2:60; :: thesis: verum