scheme :: FUNCT_2:sch 1
FuncEx1{ F1() -> set , F2() -> set , P1[ object , object ] } :
ex f being Function of F1(),F2() st
for x being object st x in F1() holds
P1[x,f . x]
provided
A1: for x being object st x in F1() holds
ex y being object st
( y in F2() & P1[x,y] )