defpred S₁[ object , object ] means ex a being Element of R st
( a = $1 & $2 = signum (P,a) );

A: now :: thesis: for x being object st x in the carrier of R holds
ex y being object st
( y in INT & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st
( y in INT & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in INT & S₁[x,y] )
then reconsider a = x as Element of R ;
thus ex y being object st
( y in INT & S₁[x,y] ) :: thesis: verum

proof

take y = signum (P,a); :: thesis: ( y in INT & S₁[x,y] )
thus ( y in INT & S₁[x,y] ) by INT_1:def 2; :: thesis: verum

end;

end;

consider f being Function of the carrier of R,INT such that
B: for x being object st x in the carrier of R holds
S₁[x,f . x] from FUNCT_2:sch 1(A);
take f ; :: thesis: for a being Element of R holds f . a = signum (P,a)

now :: thesis: for a being Element of R holds f . a = signum (P,a)

let a be Element of R; :: thesis: f . a = signum (P,a)
consider b being Element of R such that
C: ( b = a & f . a = signum (P,b) ) by B;
thus f . a = signum (P,a) by C; :: thesis: verum

end;

hence for a being Element of R holds f . a = signum (P,a) ; :: thesis: verum