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