scheme :: BINOP_2:sch 1
FuncDefUniq{ F1() -> non empty set , F2() -> non empty set , F3( Element of F1()) -> object } :
for f1, f2 being Function of F1(),F2() st ( for x being Element of F1() holds f1 . x = F3(x) ) & ( for x being Element of F1() holds f2 . x = F3(x) ) holds
f1 = f2