let f be Automorphism of G; :: according to GROUP_22:def 4 :: thesis: Image (f | ((1). G)) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #)
reconsider I = Image (f | ((1). G)) as Subgroup of (1). G by Th14;
(1). G = I by Lm8;
hence Image (f | ((1). G)) = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) ; :: thesis: verum