defpred S₁[ object , object ] 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 object st x in F₁() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st S₁[x,y] )
assume x in F₁() ; :: thesis: ex y being object 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 object st S₁[x,y]

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

end;

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

hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

end;

end;

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