defpred S₁[ object , object ] means $2 = F₂($1);
A1: for x being object st x in F₁() holds
ex y being object st S₁[x,y] ;
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