let X be set ; :: thesis: the_unity_wrt the multF of (GPFuncs X) = id X
reconsider g = id X as PartFunc of X,X ;
A1: ( g in PFuncs X,X & H₁( GPFuncs X) = PFuncs X,X ) by Def37, PARTFUN1:119;
then reconsider f = g as Element of (GPFuncs X) ;
set op = H₂( GPFuncs X);

now

let h be Element of (GPFuncs X); :: thesis: ( H₂( GPFuncs X) . f,h = h & H₂( GPFuncs X) . h,f = h )
reconsider j = h as PartFunc of X,X by A1, PARTFUN1:120;
thus H₂( GPFuncs X) . f,h = f [*] h
.= g (*) j by Def37
.= h by PARTFUN1:37 ; :: thesis: H₂( GPFuncs X) . h,f = h
thus H₂( GPFuncs X) . h,f = h [*] f
.= j (*) g by Def37
.= h by PARTFUN1:36 ; :: thesis: verum

end;

then f is_a_unity_wrt H₂( GPFuncs X) by BINOP_1:11;
hence the_unity_wrt the multF of (GPFuncs X) = id X by BINOP_1:def 8; :: thesis: verum