let A be symmetrical Subset of COMPLEX; for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
let F be PartFunc of REAL,REAL; ( F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) )
assume that
A1:
F is_even_on A
and
A2:
for x being Real st x in A holds
F . x <> 0
; ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
A3:
A c= dom F
by A1;
A4:
F | A is even
by A1;
for x being Real st x in A holds
(F . x) / (F . (- x)) = 1
proof
let x be
Real;
( x in A implies (F . x) / (F . (- x)) = 1 )
assume A5:
x in A
;
(F . x) / (F . (- x)) = 1
then A6:
x in dom (F | A)
by A3, RELAT_1:62;
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
A7:
F . x =
F /. x
by A3, A5, PARTFUN1:def 6
.=
(F | A) /. x
by A3, A5, PARTFUN2:17
.=
(F | A) . x
by A6, PARTFUN1:def 6
;
A8:
- x in A
by A5, Def1;
then A9:
- x in dom (F | A)
by A3, RELAT_1:62;
(F . x) / (F . (- x)) =
(F /. x) / (F . (- x))
by A3, A5, PARTFUN1:def 6
.=
(F /. x) / (F /. (- x))
by A3, A8, PARTFUN1:def 6
.=
((F | A) /. x) / (F /. (- x))
by A3, A5, PARTFUN2:17
.=
((F | A) /. x) / ((F | A) /. (- x))
by A3, A8, PARTFUN2:17
.=
((F | A) . x) / ((F | A) /. (- x))
by A6, PARTFUN1:def 6
.=
((F | A) . x) / ((F | A) . (- x))
by A9, PARTFUN1:def 6
.=
((F | A) . x) / ((F | A) . x)
by A4, A6, A9, Def3
.=
1
by A2, A5, A7, XCMPLX_1:60
;
hence
(F . x) / (F . (- x)) = 1
;
verum
end;
hence
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
by A1; verum