defpred S₁[ object , object ] means ( ( P₁[$1] implies $2 = F₂($1) ) & ( P₁[$1] implies $2 = F₃($1) ) );
A1: for x being object st x in F₁() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st S₁[x,y] )
( P₁[x] implies ( ( P₁[x] implies F₃(x) = F₂(x) ) & ( P₁[x] implies F₃(x) = F₃(x) ) ) ) ;
hence ( x in F₁() implies ex y being object st S₁[x,y] ) ; :: thesis: verum

end;

A2: for x, y1, y2 being object st x in F₁() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
thus ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A2, A1); :: thesis: verum