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 [:] (id D),d) * (F .: f,f9) = F .: f,((F [:] (id D),d) * 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 [:] (id D),d) * (F .: f,f9) = F .: f,((F [:] (id D),d) * f9)
let f, f9 be Function of C,D; :: thesis: for F being BinOp of D st F is associative holds
(F [:] (id D),d) * (F .: f,f9) = F .: f,((F [:] (id D),d) * f9)
let F be BinOp of D; :: thesis: ( F is associative implies (F [:] (id D),d) * (F .: f,f9) = F .: f,((F [:] (id D),d) * f9) )
assume A1: F is associative ; :: thesis: (F [:] (id D),d) * (F .: f,f9) = F .: f,((F [:] (id D),d) * f9)

now

let c be Element of C; :: thesis: ((F [:] (id D),d) * (F .: f,f9)) . c = (F .: f,((F [:] (id D),d) * f9)) . c
thus ((F [:] (id D),d) * (F .: f,f9)) . c = (F [:] (id D),d) . ((F .: f,f9) . c) by FUNCT_2:21
.= (F [:] (id D),d) . (F . (f . c),(f9 . c)) by FUNCOP_1:48
.= F . ((id D) . (F . (f . c),(f9 . c))),d by FUNCOP_1:60
.= F . (F . (f . c),(f9 . c)),d by FUNCT_1:35
.= F . (f . c),(F . (f9 . c),d) by A1, BINOP_1:def 3
.= F . (f . c),((F [:] f9,d) . c) by FUNCOP_1:60
.= F . (f . c),(((F [:] (id D),d) * f9) . c) by FUNCOP_1:63
.= (F .: f,((F [:] (id D),d) * f9)) . c by FUNCOP_1:48 ; :: thesis: verum

end;

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