let X be set ; :: thesis: ( the carrier of (MFuncs X) = Funcs X,X & the multF of (MFuncs X) = (X -composition ) || (Funcs X,X) & 1. (MFuncs X) = id X )
( the_unity_wrt H₂( GFuncs X) = id X & multMagma(# the carrier of (MFuncs X),the multF of (MFuncs X) #) = GFuncs X ) by Def22, Th84;
hence ( the carrier of (MFuncs X) = Funcs X,X & the multF of (MFuncs X) = (X -composition ) || (Funcs X,X) & 1. (MFuncs X) = id X ) by Def40, Th19, Th83; :: thesis: verum