let G be Group; :: thesis: ( (1). G is normal & (Omega). G is normal )
thus for a being Element of G holds ((1). G) |^ a = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) by Th80; :: according to GROUP_3:def 13 :: thesis: (Omega). G is normal
thus for a being Element of G holds ((Omega). G) |^ a = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) by Th82; :: according to GROUP_3:def 13 :: thesis: verum