defpred S₁[ object , object ] means ex a being Element of INT.Ring st
( $1 = a & $2 = a '*' (1. R) );
A1: for x being object st x in the carrier of INT.Ring holds
ex y being object st
( y in the carrier of R & S₁[x,y] )

proof

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

end;

consider g being Function of the carrier of INT.Ring, the carrier of R such that
A2: for x being object st x in the carrier of INT.Ring holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);

now :: thesis: for x being Element of INT.Ring holds g . x = x '*' (1. R)

let x be Element of INT.Ring; :: thesis: g . x = x '*' (1. R)
consider a being Element of INT.Ring such that
A3: ( x = a & g . x = a '*' (1. R) ) by A2;
thus g . x = x '*' (1. R) by A3; :: thesis: verum

end;

then consider f being Function of INT.Ring,R such that
A4: for x being Element of INT.Ring holds f . x = x '*' (1. R) ;
take f ; :: thesis: for x being Element of INT.Ring holds f . x = x '*' (1. R)
thus for x being Element of INT.Ring holds f . x = x '*' (1. R) by A4; :: thesis: verum