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

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

end;

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