scheme :: FRAENKEL:sch 15
Gen399{ F1() -> set , F2() -> set , F3( object , object ) -> object , P1[ object , object ], P2[ object ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : ( s in { s1 where s1 is Element of F1() : P2[s1] } & P1[s,t] ) } = { F3(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P2[s2] & P1[s2,t2] ) }