scheme :: WAYBEL_6:sch 1
NonUniqExD1{ F₁() -> non empty RelStr , F₂() -> Subset of F₁(), F₃() -> non empty Subset of F₁(), P₁[ object , object ] } :

ex f being Function of F₂(),F₃() st
for e being Element of F₁() st e in F₂() holds
ex u being Element of F₁() st
( u in F₃() & u = f . e & P₁[e,u] )

provided

A1: for e being Element of F₁() st e in F₂() holds
ex u being Element of F₁() st
( u in F₃() & P₁[e,u] )