let X be set ; :: thesis: the multF of (GFuncs X) = (X -composition) || (Funcs (X,X))
A1: H₁( GFuncs X) = Funcs (X,X) by Def40;
( H₂( GFuncs X) c= H₂( GPFuncs X) & dom H₂( GFuncs X) = [:H₁( GFuncs X),H₁( GFuncs X):] ) by Def23, FUNCT_2:def 1;
hence the multF of (GFuncs X) = (X -composition) || (Funcs (X,X)) by A1, GRFUNC_1:23; :: thesis: verum