let G be Group; :: thesis: G is Subgroup of G
dom the multF 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 multF of G = the multF of G || the carrier of G ) by RELAT_1:68; :: according to GROUP_2:def 5 :: thesis: verum