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:97; :: thesis: verum