scheme :: WAYBEL24:sch 1
FuncFraenkelSL{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } = { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] }

provided

A1: the carrier of F₂() c= dom F₄()