let C, D be non empty set ; for d being Element of D
for f, f9 being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
let d be Element of D; for f, f9 being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
let f, f9 be Function of C,D; for F being BinOp of D st F is associative holds
(F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
let F be BinOp of D; ( F is associative implies (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) )
assume A1:
F is associative
; (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
now for c being Element of C holds ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . clet c be
Element of
C;
((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . cthus ((F [;] (d,(id D))) * (F .: (f,f9))) . c =
(F [;] (d,(id D))) . ((F .: (f,f9)) . c)
by FUNCT_2:15
.=
(F [;] (d,(id D))) . (F . ((f . c),(f9 . c)))
by FUNCOP_1:37
.=
F . (
d,
((id D) . (F . ((f . c),(f9 . c)))))
by FUNCOP_1:53
.=
F . (
d,
(F . ((f . c),(f9 . c))))
.=
F . (
(F . (d,(f . c))),
(f9 . c))
by A1
.=
F . (
((F [;] (d,f)) . c),
(f9 . c))
by FUNCOP_1:53
.=
F . (
(((F [;] (d,(id D))) * f) . c),
(f9 . c))
by FUNCOP_1:55
.=
(F .: (((F [;] (d,(id D))) * f),f9)) . c
by FUNCOP_1:37
;
verum end;
hence
(F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)
by FUNCT_2:63; verum