scheme :: MODELC_1:sch 3
Func1Unique{ F₁() -> non empty set , F₂() -> Function of F₁(),BOOLEAN, F₃( object , Function of F₁(),BOOLEAN) -> boolean object } :

for g1, g2 being set st g1 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₃(s,F₂()) = TRUE iff (Fid (g1,F₁())) . s = TRUE ) ) & g2 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₃(s,F₂()) = TRUE iff (Fid (g2,F₁())) . s = TRUE ) ) holds
g1 = g2