defpred S1[ 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 & S1[x,y] )
consider f being Function of [:REALPLUS,REALPLUS:],REALPLUS such that
A3:
for x being object st x in [:REALPLUS,REALPLUS:] holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
take
f
; 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 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:];
( 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:]
;
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;
ex z being Element of REALPLUS st
( x = [y,z] & f . x = REAL_ratio (y,z) )take z =
z;
( x = [y,z] & f . x = REAL_ratio (y,z) )thus
x = [y,z]
by A4;
f . x = REAL_ratio (y,z)thus
f . x = REAL_ratio (
y,
z)
verum 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) )
; verum