defpred S₁[ object , object ] means $2 = F₃((In ($1,F₁())));
A2: for x being Element of F₁() ex y being Element of F₂() st S₁[x,y]

proof

let x be Element of F₁(); :: thesis: ex y being Element of F₂() st S₁[x,y]
reconsider y = F₃(x) as Element of F₂() by A1;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of F₁(),F₂() such that
A3: for x being Element of F₁() holds S₁[x,f . x] from FUNCT_2:sch 3(A2);
take f ; :: thesis: for x being Element of F₁() holds f . x = F₃(x)
let x be Element of F₁(); :: thesis: f . x = F₃(x)
In (x,F₁()) = x ;
hence f . x = F₃(x) by A3; :: thesis: verum