let C, D be non empty set ; :: thesis: for d being Element of D
for f, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'
let d be Element of D; :: thesis: for f, f' being Function of C,D
for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'
let f, f' be Function of C,D; :: thesis: for F being BinOp of D st F is associative holds
(F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'
let F be BinOp of D; :: thesis: ( F is associative implies (F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f' )
assume A1: F is associative ; :: thesis: (F [;] d,(id D)) * (F .: f,f') = F .: ((F [;] d,(id D)) * f),f'

now

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

end;

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