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:9;
hence the_unity_wrt the multF of (GFuncs X) = id X by Th71; :: thesis: verum