scheme :: FRAENKEL:sch 20
FrEqua2{ F1() -> set , F2() -> set , F3( object , object ) -> object , F4() -> Element of F2(), P1[ object , object ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : ( t = F4() & P1[s,t] ) } = { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }