theorem Th69: :: MONOID_0:69

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