let F, G be Function; :: thesis: ( dom F = dom f & ( for x being complex-valued Function st x in dom F holds
F . x = f . (- x) ) & dom G = dom f & ( for x being complex-valued Function st x in dom G holds
G . x = f . (- x) ) implies F = G )
assume that
A5: dom F = dom f and
A6: for x being complex-valued Function st x in dom F holds
F . x = f . (- x) and
A7: dom G = dom f and
A8: for x being complex-valued Function st x in dom G holds
G . x = f . (- x) ; :: thesis: F = G
thus dom F = dom G by A5, A7; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom F or F . b₁ = G . b₁ )
let x be set ; :: thesis: ( not x in dom F or F . x = G . x )
assume A9: x in dom F ; :: thesis: F . x = G . x
then reconsider y = x as complex-valued Function by A5;
thus F . x = f . (- y) by A6, A9
.= G . x by A5, A7, A8, A9 ; :: thesis: verum