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

end;

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