for a, b being Element of Example holds a @ b = op2 . (a,b) ;