set G = GPFuncs X;
reconsider g = id X as PartFunc of X,X ;
set D = PFuncs (X,X);
A1: the carrier of (GPFuncs X) = PFuncs (X,X) by Def37;
A2: now :: thesis: for f9, g, h being Element of (GPFuncs X) holds (f9 [*] g) [*] h = f9 [*] (g [*] h)
let f9, g, h be Element of (GPFuncs X); :: thesis: (f9 [*] g) [*] h = f9 [*] (g [*] h)
reconsider fg = f9 [*] g, gh = g [*] h as Element of (GPFuncs X) ;
thus (f9 [*] g) [*] h = h (*) fg by Def37
.= h (*) (g (*) f9) by Def37
.= (h (*) g) (*) f9 by RELAT_1:36
.= gh (*) f9 by Def37
.= f9 [*] (g [*] h) by Def37 ; :: thesis: verum
end;
reconsider f1 = g as Element of (GPFuncs X) by A1, PARTFUN1:45;
now :: thesis: for h being Element of (GPFuncs X) holds
( f1 [*] h = h & h [*] f1 = h )
let h be Element of (GPFuncs X); :: thesis: ( f1 [*] h = h & h [*] f1 = h )
reconsider j = h as PartFunc of X,X by A1, PARTFUN1:46;
thus f1 [*] h = j (*) g by Def37
.= h by PARTFUN1:6 ; :: thesis: h [*] f1 = h
thus h [*] f1 = g (*) j by Def37
.= h by PARTFUN1:7 ; :: thesis: verum
end;
hence ( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty ) by A1, A2; :: thesis: verum