let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL st F is_odd_on A holds
F " is_odd_on A
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_odd_on A implies F " is_odd_on A )
assume F is_odd_on A ; :: thesis: F " is_odd_on A
then A1: ( A c= dom F & F | A is odd ) by Def8;
A2: A c= dom (F " ) by A1, VALUED_1:def 7;
A3: dom ((F " ) | A) = A by RELAT_1:91, A2;
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; :: thesis: ( x in dom ((F " ) | A) & - x in dom ((F " ) | A) implies ((F " ) | A) . (- x) = - (((F " ) | A) . x) )
assume A5: ( x in dom ((F " ) | A) & - x in dom ((F " ) | A) ) ; :: thesis: ((F " ) | A) . (- x) = - (((F " ) | A) . x)
then A6: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, A1, A3;
((F " ) | A) . (- x) = ((F " ) | A) /. (- x) by PARTFUN1:def 8, A5
.= (F " ) /. (- x) by PARTFUN2:35, A2, A3, A5
.= (F " ) . (- x) by PARTFUN1:def 8, A2, A3, A5
.= (F . (- x)) " by VALUED_1:def 7, A2, A3, A5
.= (F /. (- x)) " by PARTFUN1:def 8, A3, A1, A5
.= ((F | A) /. (- x)) " by PARTFUN2:35, A1, A3, A5
.= ((F | A) . (- x)) " by PARTFUN1:def 8, A6
.= (- ((F | A) . x)) " by A1, Def6, A6
.= (- ((F | A) /. x)) " by PARTFUN1:def 8, A6
.= (- (F /. x)) " by PARTFUN2:35, A1, A3, A5
.= (- (F . x)) " by PARTFUN1:def 8, A1, A3, A5
.= - ((F . x) " ) by XCMPLX_1:224
.= - ((F " ) . x) by VALUED_1:def 7, A2, A3, A5
.= - ((F " ) /. x) by PARTFUN1:def 8, A2, A3, A5
.= - (((F " ) | A) /. x) by PARTFUN2:35, A2, A3, A5
.= - (((F " ) | A) . x) by PARTFUN1:def 8, A5 ;
hence ((F " ) | A) . (- x) = - (((F " ) | A) . x) ; :: thesis: verum

end;

then ( (F " ) | A is with_symmetrical_domain & (F " ) | A is quasi_odd ) by Def6, A3, Def2;
hence F " is_odd_on A by A2, Def8; :: thesis: verum