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

proof

let x be Real; :: thesis: ( x in dom (r (#) F) & - x in dom (r (#) F) implies (r (#) F) . (- x) = - ((r (#) F) . x) )
assume A3: ( x in dom (r (#) F) & - x in dom (r (#) F) ) ; :: thesis: (r (#) F) . (- x) = - ((r (#) F) . x)
(r (#) F) . (- x) = r * (F . (- x)) by A3, VALUED_1:def 5
.= r * (- (F . x)) by A1, Def6, A2, A3
.= - (r * (F . x))
.= - ((r (#) F) . x) by A3, VALUED_1:def 5 ;
hence (r (#) F) . (- x) = - ((r (#) F) . x) ; :: thesis: verum

end;

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