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))

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 :: thesis: for c being Element of C holds ((F * ((id D),u)) .: (f,f9)) . c = (F .: (f,(u * f9))) . c

hence
(F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9))
by FUNCT_2:63; :: thesis: verumlet 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:37

.= F . ((f . c),(u . (f9 . c))) by Th81

.= F . ((f . c),((u * f9) . c)) by FUNCT_2:15

.= (F .: (f,(u * f9))) . c by FUNCOP_1:37 ; :: thesis: verum

end;thus ((F * ((id D),u)) .: (f,f9)) . c = (F * ((id D),u)) . ((f . c),(f9 . c)) by FUNCOP_1:37

.= F . ((f . c),(u . (f9 . c))) by Th81

.= F . ((f . c),((u * f9) . c)) by FUNCT_2:15

.= (F .: (f,(u * f9))) . c by FUNCOP_1:37 ; :: thesis: verum