let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL st F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) ) )
assume A1: ( F is_odd_on A & ( for x being Real st x in A holds
F . x <> 0 ) ) ; :: thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) )
then A2: ( A c= dom F & F | A is odd ) by Def8;
for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1

proof

let x be Real; :: thesis: ( x in A implies (F . x) / (F . (- x)) = - 1 )
assume A5: x in A ; :: thesis: (F . x) / (F . (- x)) = - 1
then A4: ( x in A & - x in A ) by Def1;
then A6: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, A2;
A7: F . x = F /. x by A2, A5, PARTFUN1:def 8
.= (F | A) /. x by PARTFUN2:35, A2, A5
.= (F | A) . x by PARTFUN1:def 8, A6 ;
(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A2, A5, PARTFUN1:def 8
.= (F /. x) / (F /. (- x)) by A2, A4, PARTFUN1:def 8
.= ((F | A) /. x) / (F /. (- x)) by PARTFUN2:35, A2, A5
.= ((F | A) /. x) / ((F | A) /. (- x)) by PARTFUN2:35, A2, A4
.= ((F | A) . x) / ((F | A) /. (- x)) by PARTFUN1:def 8, A6
.= ((F | A) . x) / ((F | A) . (- x)) by PARTFUN1:def 8, A6
.= ((F | A) . x) / (- ((F | A) . x)) by A2, A6, Def6
.= - (((F | A) . x) / ((F | A) . x)) by XCMPLX_1:189
.= - 1 by XCMPLX_1:60, A1, A5, A7 ;
hence (F . x) / (F . (- x)) = - 1 ; :: thesis: verum

end;

hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = - 1 ) ) by A1, Def8; :: thesis: verum