let C, D be non empty set ; :: thesis: for f, f9 being Function of C,D
for F being BinOp of D
for u being UnOp of D holds (F * (id D),u) .: f,f9 = F .: f,(u * f9)
let f, f9 be Function of C,D; :: thesis: for F being BinOp of D
for u being UnOp of D holds (F * (id D),u) .: f,f9 = F .: f,(u * f9)
let F be BinOp of D; :: thesis: for u being UnOp of D holds (F * (id D),u) .: f,f9 = F .: f,(u * f9)
let u be UnOp of D; :: thesis: (F * (id D),u) .: f,f9 = F .: f,(u * f9)

now

let c be Element of C; :: thesis: ((F * (id D),u) .: f,f9) . c = (F .: f,(u * f9)) . c
thus ((F * (id D),u) .: f,f9) . c = (F * (id D),u) . (f . c),(f9 . c) by FUNCOP_1:48
.= F . (f . c),(u . (f9 . c)) by Th87
.= F . (f . c),((u * f9) . c) by FUNCT_2:21
.= (F .: f,(u * f9)) . c by FUNCOP_1:48 ; :: thesis: verum

end;

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