theorem Th71: :: MONOID_0:71

for X being set
for F being non empty SubStr of GPFuncs X st id X is Element of F holds
( F is unital & the_unity_wrt the multF of F = id X )