let f, g be Function; ( 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)
; f = g
hence
f = g
by A2, A4, FUNCT_1:2; verum