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