let g, h be Function; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = cot (f . x) ) & dom h = dom f & ( for x being object st x in dom f holds
h . x = cot (f . x) ) implies g = h )
assume that
A1: dom g = dom f and
A2: for x being object st x in dom f holds
g . x = cot (f . x) and
A3: dom h = dom f and
A4: for x being object st x in dom f holds
h . x = cot (f . x) ; :: thesis: g = h
thus dom g = dom h by A1, A3; :: 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 A5: x in dom g ; :: thesis: g . x = h . x
thus g . x = cot (f . x) by A1, A2, A5
.= h . x by A1, A4, A5 ; :: thesis: verum