defpred S1[ object , object ] means ( $1 in F1() & P1[$1,$2] );
A3:
for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2
by A1;
consider f being Function such that
A4:
for x, y being object holds
( [x,y] in f iff ( x in F1() & S1[x,y] ) )
from FUNCT_1:sch 1(A3);
take
f
; ( dom f = F1() & ( for x being object st x in F1() holds
P1[x,f . x] ) )
for x being object holds
( x in dom f iff x in F1() )
hence A7:
dom f = F1()
by TARSKI:2; for x being object st x in F1() holds
P1[x,f . x]
let x be object ; ( x in F1() implies P1[x,f . x] )
assume A8:
x in F1()
; P1[x,f . x]
then consider y being object such that
A9:
P1[x,y]
by A2;
reconsider y = y as set by TARSKI:1;
[x,y] in f
by A4, A8, A9;
hence
P1[x,f . x]
by A7, A8, A9, Def2; verum