take G ; :: thesis: ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier 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; :: thesis: verum