let f1, f2 be Function of [:REALPLUS,REALPLUS:],REALPLUS; ( ( 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) )
; f1 = f2
now ( 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;
for x being object st x in dom f1 holds
f1 . x = f2 . xhereby verum
let x be
object ;
( x in dom f1 implies f1 . x = f2 . x )assume
x in dom f1
;
f1 . x = f2 . xthen 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;
verum
end; end;
hence
f1 = f2
by FUNCT_1:2; verum