theorem Th75: :: MONOID_0:75

for X being set holds the_unity_wrt the multF of (GFuncs X) = id X