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

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

hence
g = h
by A1, A3, FUNCT_1:2; :: thesis: verumg . 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;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