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

now :: thesis: for h being Element of (GPFuncs X) holds
( H₂( GPFuncs X) . (f,h) = h & H₂( GPFuncs X) . (h,f) = h )

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:46;
thus H₂( GPFuncs X) . (f,h) = f [*] h
.= j (*) g by Def37
.= h by PARTFUN1:6 ; :: thesis: H₂( GPFuncs X) . (h,f) = h
thus H₂( GPFuncs X) . (h,f) = h [*] f
.= g (*) j by Def37
.= h by PARTFUN1:7 ; :: thesis: verum

end;

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