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

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