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

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

provided

A1: for x, y being Element of F₁() st [x,y] in F₃() holds
[F₂(x),F₂(y)] in F₃()