let g, h be Function; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = ].((f . x) - r),((f . x) + r).[ ) & dom h = dom f & ( for x being object st x in dom f holds
h . x = ].((f . x) - r),((f . x) + r).[ ) implies g = h )
assume that
A1: dom g = dom f and
A2: for x being object st x in dom f holds
g . x = ].((f . x) - r),((f . x) + r).[ and
A3: dom h = dom f and
A4: for x being object st x in dom f holds
h . x = ].((f . x) - r),((f . x) + r).[ ; :: thesis: g = h

now :: thesis: for x being object st x in dom g holds
g . x = h . x

let x be object ; :: thesis: ( x in dom g implies g . x = h . x )
assume A5: x in dom g ; :: thesis: g . x = h . x
hence g . x = ].((f . x) - r),((f . x) + r).[ by A1, A2
.= h . x by A1, A4, A5 ;
:: thesis: verum

end;

hence g = h by A1, A3, FUNCT_1:2; :: thesis: verum