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

proof

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

end;

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

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

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

proof

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

end;

end;

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