scheme :: SCHEME1:sch 8
PartFuncExD299{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } :
ex f being PartFunc of F1(),F2() st
( f is total & ( for c being Element of F1() st c in dom f holds
( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) ) )