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 and
A3: for r being Element of REAL holds f . r = Replace (x,i,r) and
A4: dom g = REAL and
A5: for r being Element of REAL holds g . r = Replace (x,i,r) ; :: thesis: f = g

now :: thesis: for p being object st p in dom f holds
f . p = g . p

let p be object ; :: 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 A3;
hence f . p = g . p by A5; :: thesis: verum

end;

hence f = g by A2, A4, FUNCT_1:2; :: thesis: verum