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:8;
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 VALUED_1:8
.= - (- (F . x)) by A1, Def6, A2, A3
.= - ((- F) . x) by VALUED_1:8 ;
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