let r be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( F is_odd_on A implies r (#) F is_odd_on A )
assume A1: F is_odd_on A ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ((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) ; :: thesis: 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; :: thesis: verum