scheme :: CARDFIN2:sch 1
FraenkelDiff{ F₁() -> set , F₂() -> set , P₁[ object ] } :

{ f where f is Function of F₁(),F₂() : P₁[f] } = (Funcs (F₁(),F₂())) \ { f where f is Function of F₁(),F₂() : P₁[f] }

provided

A1: ( F₂() = {} implies F₁() = {} )