defpred S₁[ set , set ] means ( ( $1 = F₃() implies $2 = F₄() ) & ( $1 <> F₃() implies $2 = F₅($1) ) );
A1: 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]
( x = F₃() implies ex y being Element of F₂() st S₁[x,y] ) ;
hence ex y being Element of F₂() st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of F₁(),F₂() such that
A2: for x being Element of F₁() holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: ( f . F₃() = F₄() & ( for x being Element of F₁() st x <> F₃() holds
f . x = F₅(x) ) )
thus ( f . F₃() = F₄() & ( for x being Element of F₁() st x <> F₃() holds
f . x = F₅(x) ) ) by A2; :: thesis: verum