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 ;
consider f being Function such that
A3: dom f = F₁() and
A4: for x being object st x in F₁() holds
S₁[x,f . x] from FUNCT_1:sch 2(A2, A1);
take f ; :: thesis: ( dom f = F₁() & ( for X being set st X in F₁() holds
f . X = F₂(X) ) )
thus dom f = F₁() by A3; :: thesis: for X being set st X in F₁() holds
f . X = F₂(X)
thus for X being set st X in F₁() holds
f . X = F₂(X) by A4; :: thesis: verum