let F be PartFunc of REAL ,REAL ; :: thesis: ( F is odd implies F " is odd )
assume A1: F is odd ; :: thesis: F " is odd
A2: dom F = dom (F " ) by VALUED_1:def 7;
for x being Real st x in dom (F " ) & - x in dom (F " ) holds
(F " ) . (- x) = - ((F " ) . x)

proof

let x be Real; :: thesis: ( x in dom (F " ) & - x in dom (F " ) implies (F " ) . (- x) = - ((F " ) . x) )
assume A3: ( x in dom (F " ) & - x in dom (F " ) ) ; :: thesis: (F " ) . (- x) = - ((F " ) . x)
(F " ) . (- x) = (F . (- x)) " by A3, VALUED_1:def 7
.= (- (F . x)) " by A1, Def6, A2, A3
.= - ((F . x) " ) by XCMPLX_1:224
.= - ((F " ) . x) by A3, VALUED_1:def 7 ;
hence (F " ) . (- x) = - ((F " ) . x) ; :: thesis: verum

end;

then ( F " is with_symmetrical_domain & F " is quasi_odd ) by Def6, A1, A2, Def2;
hence F " is odd ; :: thesis: verum