let C, E, D 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

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:21
.= h . (F . (f . c),(f9 . c)) by FUNCOP_1:48
.= H . (h . (f . c)),(h . (f9 . c)) by A1
.= H . ((h * f) . c),(h . (f9 . c)) by FUNCT_2:21
.= H . ((h * f) . c),((h * f9) . c) by FUNCT_2:21
.= (H .: (h * f),(h * f9)) . c by FUNCOP_1:48 ; :: thesis: verum

end;

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