let C, E, D be non empty set ; :: thesis: for f, f' 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,f') = H .: (h * f),(h * f')
let f, f' 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,f') = H .: (h * f),(h * f')
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,f') = H .: (h * f),(h * f')
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,f') = H .: (h * f),(h * f')
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,f') = H .: (h * f),(h * f') )
assume A1: for d1, d2 being Element of D holds h . (F . d1,d2) = H . (h . d1),(h . d2) ; :: thesis: h * (F .: f,f') = H .: (h * f),(h * f')

now

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

end;

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