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

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

hence
f = g
by A2, A4, FUNCT_1:2; :: thesis: verumf . 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;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