scheme :: GRZLOG_1:sch 3
BinOpCongr{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁()) -> Element of F₁(), F₃() -> Equivalence_Relation of F₁() } :

ex f being BinOp of (Class F₃()) st
for x, y being Element of F₁() holds f . ((Class (F₃(),x)),(Class (F₃(),y))) = Class (F₃(),F₂(x,y))

provided

A1: for x1, x2, y1, y2 being Element of F₁() st [x1,x2] in F₃() & [y1,y2] in F₃() holds
[F₂(x1,y1),F₂(x2,y2)] in F₃()