scheme :: TOPGEN_5:sch 1
SCH1{ P₁[ object ], F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( object ) -> set , F₅( object ) -> set } :

ex f being Function of F₃(),F₂() st
for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies f . a = F₄(a) ) & ( P₁[a] implies f . a = F₅(a) ) )

provided

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