defpred S1[ object , object ] means ( ( P1[$1] implies $2 = F2($1) ) & ( P1[$1] implies $2 = F3($1) ) );
A1:
for x being object st x in F1() holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in F1() implies ex y being object st S1[x,y] )
(
P1[
x] implies ( (
P1[
x] implies
F3(
x)
= F2(
x) ) & (
P1[
x] implies
F3(
x)
= F3(
x) ) ) )
;
hence
(
x in F1() implies ex
y being
object st
S1[
x,
y] )
;
verum
end;
A2:
for x, y1, y2 being object st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2
;
thus
ex f being Function st
( dom f = F1() & ( for x being object st x in F1() holds
S1[x,f . x] ) )
from FUNCT_1:sch 2(A2, A1); verum