let f1, f2 be Function of [:REALPLUS,REALPLUS:],REALPLUS; :: thesis: ( ( for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f1 . x = REAL_ratio (y,z) ) ) & ( for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f2 . x = REAL_ratio (y,z) ) ) implies f1 = f2 )
assume that
A6: for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f1 . x = REAL_ratio (y,z) ) and
A7: for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & f2 . x = REAL_ratio (y,z) ) ; :: thesis: f1 = f2

now :: thesis: ( dom f1 = dom f2 & ( for x being object st x in dom f1 holds
f1 . x = f2 . x ) )

dom f1 = [:REALPLUS,REALPLUS:] by PARTFUN1:def 2;
hence dom f1 = dom f2 by PARTFUN1:def 2; :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider y = x as Element of [:REALPLUS,REALPLUS:] ;
consider z, t being Element of REALPLUS such that
A8: ( y = [z,t] & f1 . y = REAL_ratio (z,t) ) by A6;
consider z9, t9 being Element of REALPLUS such that
A9: ( y = [z9,t9] & f2 . y = REAL_ratio (z9,t9) ) by A7;
( z = z9 & t = t9 ) by A8, A9, XTUPLE_0:1;
hence f1 . x = f2 . x by A8, A9; :: thesis: verum

end;

end;

hence f1 = f2 by FUNCT_1:2; :: thesis: verum