scheme :: FUNCT_2:sch 3
FuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ object , object ] } :
ex f being Function of F1(),F2() st
for x being Element of F1() holds P1[x,f . x]
provided
A1: for x being Element of F1() ex y being Element of F2() st P1[x,y]