scheme :: CARDFIN2:sch 1
FraenkelDiff{ F1() -> set , F2() -> set , P1[ object ] } :
{ f where f is Function of F1(),F2() : P1[f] } = (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
provided
A1: ( F2() = {} implies F1() = {} )