let g, h be Function; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = cosec (f . x) ) & dom h = dom f & ( for x being object st x in dom f holds
h . x = cosec (f . x) ) implies g = h )
assume that
A6: dom g = dom f and
A7: for x being object st x in dom f holds
g . x = cosec (f . x) and
A8: dom h = dom f and
A9: for x being object st x in dom f holds
h . x = cosec (f . x) ; :: thesis: g = h
thus dom g = dom h by A6, A8; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom g or g . b₁ = h . b₁ )
let x be object ; :: thesis: ( not x in dom g or g . x = h . x )
assume A10: x in dom g ; :: thesis: g . x = h . x
thus g . x = cosec (f . x) by A6, A7, A10
.= h . x by A6, A9, A10 ; :: thesis: verum