reconsider g = id X as PartFunc of X,X ;
set D = PFuncs (X,X);
defpred S1[ Element of PFuncs (X,X), Element of PFuncs (X,X), Element of PFuncs (X,X)] means ex f, g being PartFunc of X,X st
( $1 = f & $2 = g & $3 = g (*) f );
A1:
for a, b being Element of PFuncs (X,X) ex c being Element of PFuncs (X,X) st S1[a,b,c]
proof
let a,
b be
Element of
PFuncs (
X,
X);
ex c being Element of PFuncs (X,X) st S1[a,b,c]
reconsider f =
a,
g =
b as
PartFunc of
X,
X by PARTFUN1:46;
reconsider c =
g * f as
Element of
PFuncs (
X,
X)
by PARTFUN1:45;
take
c
;
S1[a,b,c]
take
f
;
ex g being PartFunc of X,X st
( a = f & b = g & c = g (*) f )
take
g
;
( a = f & b = g & c = g (*) f )
thus
(
a = f &
b = g &
c = g (*) f )
;
verum
end;
consider f being BinOp of (PFuncs (X,X)) such that
A2:
for a, b being Element of PFuncs (X,X) holds S1[a,b,f . (a,b)]
from BINOP_1:sch 3(A1);
set G = multMagma(# (PFuncs (X,X)),f #);
multMagma(# (PFuncs (X,X)),f #) is constituted-Functions
;
then reconsider G = multMagma(# (PFuncs (X,X)),f #) as strict constituted-Functions multMagma ;
take
G
; ( the carrier of G = PFuncs (X,X) & ( for f, g being Element of G holds f [*] g = g (*) f ) )
thus
H1(G) = PFuncs (X,X)
; for f, g being Element of G holds f [*] g = g (*) f
let g, h be Element of G; g [*] h = h (*) g
reconsider g9 = g, h9 = h as Element of PFuncs (X,X) ;
ex g, h being PartFunc of X,X st
( g9 = g & h9 = h & f . (g9,h9) = h (*) g )
by A2;
hence
g [*] h = h (*) g
; verum