let C, D, E be non empty set ; :: thesis: for f, f9 being Function of C,D
for h being Function of D,E
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h * (F .: (f,f9)) = H .: ((h * f),(h * f9))
let f, f9 be Function of C,D; :: thesis: for h being Function of D,E
for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h * (F .: (f,f9)) = H .: ((h * f),(h * f9))
let h be Function of D,E; :: thesis: for F being BinOp of D
for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h * (F .: (f,f9)) = H .: ((h * f),(h * f9))
let F be BinOp of D; :: thesis: for H being BinOp of E st ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h * (F .: (f,f9)) = H .: ((h * f),(h * f9))
let H be BinOp of E; :: thesis: ( ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) )
assume A1: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; :: thesis: h * (F .: (f,f9)) = H .: ((h * f),(h * f9))

now :: thesis: for c being Element of C holds (h * (F .: (f,f9))) . c = (H .: ((h * f),(h * f9))) . c

let c be Element of C; :: thesis: (h * (F .: (f,f9))) . c = (H .: ((h * f),(h * f9))) . c
thus (h * (F .: (f,f9))) . c = h . ((F .: (f,f9)) . c) by FUNCT_2:15
.= h . (F . ((f . c),(f9 . c))) by FUNCOP_1:37
.= H . ((h . (f . c)),(h . (f9 . c))) by A1
.= H . (((h * f) . c),(h . (f9 . c))) by FUNCT_2:15
.= H . (((h * f) . c),((h * f9) . c)) by FUNCT_2:15
.= (H .: ((h * f),(h * f9))) . c by FUNCOP_1:37 ; :: thesis: verum

end;

hence h * (F .: (f,f9)) = H .: ((h * f),(h * f9)) by FUNCT_2:63; :: thesis: verum