defpred S₁[ object , object ] means ex x, y being Element of REALPLUS st
( $1 = [x,y] & $2 = REAL_ratio (x,y) );
A1: for x being object st x in [:REALPLUS,REALPLUS:] holds
ex y being object st
( y in REALPLUS & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in [:REALPLUS,REALPLUS:] implies ex y being object st
( y in REALPLUS & S₁[x,y] ) )
assume x in [:REALPLUS,REALPLUS:] ; :: thesis: ex y being object st
( y in REALPLUS & S₁[x,y] )
then consider y, z being object such that
A2: ( y in REALPLUS & z in REALPLUS & x = [y,z] ) by ZFMISC_1:def 2;
reconsider y = y, z = z as Element of REALPLUS by A2;
REAL_ratio (y,z) is Element of REALPLUS ;
hence ex y being object st
( y in REALPLUS & S₁[x,y] ) by A2; :: thesis: verum

end;

consider f being Function of [:REALPLUS,REALPLUS:],REALPLUS such that
A3: for x being object st x in [:REALPLUS,REALPLUS:] holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) )

now :: thesis: for x being Element of [:REALPLUS,REALPLUS:] st x is Element of [:REALPLUS,REALPLUS:] holds
ex y, z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) )

let x be Element of [:REALPLUS,REALPLUS:]; :: thesis: ( x is Element of [:REALPLUS,REALPLUS:] implies ex y, z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) ) )
assume x is Element of [:REALPLUS,REALPLUS:] ; :: thesis: ex y, z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) )
consider y, z being object such that
A4: ( y in REALPLUS & z in REALPLUS & x = [y,z] ) by ZFMISC_1:def 2;
reconsider y = y, z = z as Element of REALPLUS by A4;
take y = y; :: thesis: ex z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) )
take z = z; :: thesis: ( x = [y,z] & f . x = REAL_ratio (y,z) )
thus x = [y,z] by A4; :: thesis: f . x = REAL_ratio (y,z)
thus f . x = REAL_ratio (y,z) :: thesis: verum

proof

consider x9, y9 being Element of REALPLUS such that
A5: ( x = [x9,y9] & f . x = REAL_ratio (x9,y9) ) by A3;
( x9 = y & y9 = z ) by A4, A5, XTUPLE_0:1;
hence f . x = REAL_ratio (y,z) by A5; :: thesis: verum

end;

end;

hence for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) ) ; :: thesis: verum