for D, E being non empty set
for F being BinOp of D
for H being BinOp of E
for h being Function of D,E
for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds
h . (F "**" p) = H "**" (h * p)