let G be addGroup; :: thesis: G is Subgroup of G
dom the addF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
hence ( the carrier of G c= the carrier of G & the addF of G = the addF of G || the carrier of G ) by RELAT_1:68; :: according to GROUP_1A:def 15 :: thesis: verum