let F be PartFunc of REAL,REAL; :: thesis: ( F is odd implies F " is odd )

A1: dom F = dom (F ") by VALUED_1:def 7;

assume A2: F is odd ; :: thesis: F " is odd

for x being Real st x in dom (F ") & - x in dom (F ") holds

(F ") . (- x) = - ((F ") . x)

hence F " is odd ; :: thesis: verum

A1: dom F = dom (F ") by VALUED_1:def 7;

assume A2: F is odd ; :: thesis: F " is odd

for x being Real st x in dom (F ") & - x in dom (F ") holds

(F ") . (- x) = - ((F ") . x)

proof

then
( F " is with_symmetrical_domain & F " is quasi_odd )
by A2, A1;
let x be Real; :: thesis: ( x in dom (F ") & - x in dom (F ") implies (F ") . (- x) = - ((F ") . x) )

assume that

A3: x in dom (F ") and

A4: - x in dom (F ") ; :: thesis: (F ") . (- x) = - ((F ") . x)

(F ") . (- x) = (F . (- x)) " by A4, VALUED_1:def 7

.= (- (F . x)) " by A2, A1, A3, A4, Def6

.= - ((F . x) ") by XCMPLX_1:222

.= - ((F ") . x) by A3, VALUED_1:def 7 ;

hence (F ") . (- x) = - ((F ") . x) ; :: thesis: verum

end;assume that

A3: x in dom (F ") and

A4: - x in dom (F ") ; :: thesis: (F ") . (- x) = - ((F ") . x)

(F ") . (- x) = (F . (- x)) " by A4, VALUED_1:def 7

.= (- (F . x)) " by A2, A1, A3, A4, Def6

.= - ((F . x) ") by XCMPLX_1:222

.= - ((F ") . x) by A3, VALUED_1:def 7 ;

hence (F ") . (- x) = - ((F ") . x) ; :: thesis: verum

hence F " is odd ; :: thesis: verum