scheme :: PARTFUN2:sch 1
PartFuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ object , object ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )