scheme :: PARTFUN1:sch 4
LambdaC9{ F1() -> non empty set , P1[ object ], F2( object ) -> object , F3( object ) -> object } :
ex f being Function st
( dom f = F1() & ( for x being Element of F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )