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

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

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