let f, g be Function; :: thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace x,i,r ) & dom g = REAL & ( for r being Element of REAL holds g . r = Replace x,i,r ) implies f = g )
assume that
A2: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace x,i,r ) ) and
A3: ( dom g = REAL & ( for r being Element of REAL holds g . r = Replace x,i,r ) ) ; :: thesis: f = g

now

let p be set ; :: thesis: ( p in dom f implies f . p = g . p )
assume p in dom f ; :: thesis: f . p = g . p
then reconsider r = p as Element of REAL by A2;
f . r = Replace x,i,r by A2;
hence f . p = g . p by A3; :: thesis: verum

end;

hence f = g by A2, A3, FUNCT_1:9; :: thesis: verum