theorem Th78: :: MONOID_0:78

for X being set holds
( the_unity_wrt the multF of (GPerms X) = id X & 1_ (GPerms X) = id X )