let C, D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( F is associative implies (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) )
assume A1: F is associative ; :: thesis: (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)

now :: thesis: for c being Element of C holds ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . c

let c be Element of C; :: thesis: ((F [;] (d,(id D))) * (F .: (f,f9))) . c = (F .: (((F [;] (d,(id D))) * f),f9)) . c
thus ((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 ; :: thesis: verum

end;

hence (F [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9) by FUNCT_2:63; :: thesis: verum