let A be symmetrical Subset of COMPLEX; for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) holds
F is_odd_on A
let F be PartFunc of REAL,REAL; ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) implies F is_odd_on A )
assume that
A1:
A c= dom F
and
A2:
for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1
; F is_odd_on A
A3:
dom (F | A) = A
by A1, RELAT_1:62;
A4:
for x being Real st x in A holds
F . (- x) = - (F . x)
for x being Real st x in dom (F | A) & - x in dom (F | A) holds
(F | A) . (- x) = - ((F | A) . x)
proof
let x be
Real;
( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = - ((F | A) . x) )
assume that A5:
x in dom (F | A)
and A6:
- x in dom (F | A)
;
(F | A) . (- x) = - ((F | A) . x)
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
(F | A) . (- x) =
(F | A) /. (- x)
by A6, PARTFUN1:def 6
.=
F /. (- x)
by A1, A3, A6, PARTFUN2:17
.=
F . (- x)
by A1, A6, PARTFUN1:def 6
.=
- (F . x)
by A4, A5
.=
- (F /. x)
by A1, A5, PARTFUN1:def 6
.=
- ((F | A) /. x)
by A1, A3, A5, PARTFUN2:17
.=
- ((F | A) . x)
by A5, PARTFUN1:def 6
;
hence
(F | A) . (- x) = - ((F | A) . x)
;
verum
end;
then
( F | A is with_symmetrical_domain & F | A is quasi_odd )
by A3;
hence
F is_odd_on A
by A1; verum