let X be set ; :: thesis: the_unity_wrt the multF of (GFuncs X) = id X
( id X in Funcs X,X & H₁( GFuncs X) = Funcs X,X ) by Def40, FUNCT_2:12;
hence the_unity_wrt the multF of (GFuncs X) = id X by Th80; :: thesis: verum