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
A4: dom F = dom f and
A5: for x being complex-valued Function st x in dom F holds
F . x = f . (- x) and
A6: dom G = dom f and
A7: 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 A4, A6; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom F or F . b₁ = G . b₁ )
let x be object ; :: thesis: ( not x in dom F or F . x = G . x )
assume A8: x in dom F ; :: thesis: F . x = G . x
then reconsider y = x as complex-valued Function by A4;
thus F . x = f . (- y) by A5, A8
.= G . x by A4, A6, A7, A8 ; :: thesis: verum