:: deftheorem defines lift_binary_op NOMIN_4:def 8 :
for V, A being set
for a, b being Element of V
for op being Function of [:A,A:],A holds lift_binary_op (op,a,b) = op * <:(denaming (V,A,a)),(denaming (V,A,b)):>;