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, Th75;
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, Th17, Th74; :: thesis: verum