let F be PartFunc of REAL,REAL; :: thesis: ( F is odd implies - F is odd )
A1: dom F = dom (- F) by VALUED_1:8;
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

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 A2, A1, A3, Def6
.= - ((- 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 A2, A1;
hence - F is odd ; :: thesis: verum