scheme :: RECDEF_2:sch 2
ExFunc4Cond{ F₁() -> set , P₁[ object ], P₂[ object ], P₃[ object ], P₄[ object ], F₂( object ) -> object , F₃( object ) -> object , F₄( object ) -> object , F₅( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for c being set st c in F₁() holds
( ( P₁[c] implies f . c = F₂(c) ) & ( 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 set st c in F₁() holds
( ( P₁[c] implies not P₂[c] ) & ( P₁[c] implies not P₃[c] ) & ( P₁[c] implies not P₄[c] ) & ( P₂[c] implies not P₃[c] ) & ( P₂[c] implies not P₄[c] ) & ( P₃[c] implies not P₄[c] ) ) and
A2: for c being set holds
( not c in F₁() or P₁[c] or P₂[c] or P₃[c] or P₄[c] )