defpred S₁[ set , set ] means ( ( $1 is Element of F₂() implies ex x being Element of F₂() st
( x = $1 & $2 = F₃(x) ) ) & ( $1 is not Element of F₂() implies $2 = 0 ) );
A1: for x being set st x in F₁() holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F₁() implies ex y being set st S₁[x,y] )
assume x in F₁() ; :: thesis: ex y being set st S₁[x,y]

per cases ( x is Element of F₂() or not x is Element of F₂() ) ;

suppose x is Element of F₂() ; :: thesis: ex y being set st S₁[x,y]

then reconsider z = x as Element of F₂() ;
take y = F₃(z); :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

suppose A2: x is not Element of F₂() ; :: thesis: ex y being set st S₁[x,y]

take y = 0 ; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

end;

end;

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
then consider f being Function such that
A3: dom f = F₁() and
A4: for x being set st x in F₁() holds
S₁[x,f . x] ;
take f ; :: thesis: ( dom f = F₁() & ( for x being Element of F₂() st x in F₁() holds
f . x = F₃(x) ) )

now

let x be Element of F₂(); :: thesis: ( x in F₁() implies f . x = F₃(x) )
assume x in F₁() ; :: thesis: f . x = F₃(x)
then S₁[x,f . x] by A4;
hence f . x = F₃(x) ; :: thesis: verum

end;

hence ( dom f = F₁() & ( for x being Element of F₂() st x in F₁() holds
f . x = F₃(x) ) ) by A3; :: thesis: verum