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