scheme :: SCHEME1:sch 10
PartFuncExD39{ F₁() -> non empty set , F₂() -> non empty set , P₁[ object ], P₂[ object ], P₃[ object ], F₃( object ) -> Element of F₂(), F₄( object ) -> Element of F₂(), F₅( object ) -> Element of F₂() } :

ex f being PartFunc of F₁(),F₂() st
( ( for c being Element of F₁() holds
( c in dom f iff ( P₁[c] or P₂[c] or P₃[c] ) ) ) & ( for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( P₂[c] implies f . c = F₄(c) ) & ( P₃[c] implies f . c = F₅(c) ) ) ) )

provided

A1: for c being Element of F₁() holds
( ( P₁[c] & P₂[c] implies F₃(c) = F₄(c) ) & ( P₁[c] & P₃[c] implies F₃(c) = F₅(c) ) & ( P₂[c] & P₃[c] implies F₄(c) = F₅(c) ) )