scheme :: SETWISEO:sch 1
FinSubFuncEx{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ set , set ] } :
ex f being Function of F1(),(Fin F1()) st
for b, a being Element of F1() holds
( a in f . b iff ( a in F2() & P1[a,b] ) )