scheme :: ROUGHIF1:sch 1
BinOpEq{ F1() -> non empty 1-sorted , F2( Subset of F1(), Subset of F1()) -> Element of [.0,1.] } :
for f1, f2 being preRIF of F1() st ( for x, y being Subset of F1() holds f1 . (x,y) = F2(x,y) ) & ( for x, y being Subset of F1() holds f2 . (x,y) = F2(x,y) ) holds
f1 = f2