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 that

A1: F is_odd_on A and

A2: 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 ) )

A3: A c= dom F by A1;

A4: F | A is odd by A1;

for x being Real st x in A holds

(F . x) / (F . (- x)) = - 1

(F . x) / (F . (- x)) = - 1 ) ) by A1; :: thesis: verum

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 that

A1: F is_odd_on A and

A2: 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 ) )

A3: A c= dom F by A1;

A4: F | A is odd by A1;

for x being Real st x in A holds

(F . x) / (F . (- x)) = - 1

proof

hence
( A c= dom F & ( for x being Real st x in A holds
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 A6: x in dom (F | A) by A3, RELAT_1:62;

reconsider x = x as Element of REAL by XREAL_0:def 1;

A7: F . x = F /. x by A3, A5, PARTFUN1:def 6

.= (F | A) /. x by A3, A5, PARTFUN2:17

.= (F | A) . x by A6, PARTFUN1:def 6 ;

A8: - x in A by A5, Def1;

then A9: - x in dom (F | A) by A3, RELAT_1:62;

(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A3, A5, PARTFUN1:def 6

.= (F /. x) / (F /. (- x)) by A3, A8, PARTFUN1:def 6

.= ((F | A) /. x) / (F /. (- x)) by A3, A5, PARTFUN2:17

.= ((F | A) /. x) / ((F | A) /. (- x)) by A3, A8, PARTFUN2:17

.= ((F | A) . x) / ((F | A) /. (- x)) by A6, PARTFUN1:def 6

.= ((F | A) . x) / ((F | A) . (- x)) by A9, PARTFUN1:def 6

.= ((F | A) . x) / (- ((F | A) . x)) by A4, A6, A9, Def6

.= - (((F | A) . x) / ((F | A) . x)) by XCMPLX_1:188

.= - 1 by A2, A5, A7, XCMPLX_1:60 ;

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

end;assume A5: x in A ; :: thesis: (F . x) / (F . (- x)) = - 1

then A6: x in dom (F | A) by A3, RELAT_1:62;

reconsider x = x as Element of REAL by XREAL_0:def 1;

A7: F . x = F /. x by A3, A5, PARTFUN1:def 6

.= (F | A) /. x by A3, A5, PARTFUN2:17

.= (F | A) . x by A6, PARTFUN1:def 6 ;

A8: - x in A by A5, Def1;

then A9: - x in dom (F | A) by A3, RELAT_1:62;

(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A3, A5, PARTFUN1:def 6

.= (F /. x) / (F /. (- x)) by A3, A8, PARTFUN1:def 6

.= ((F | A) /. x) / (F /. (- x)) by A3, A5, PARTFUN2:17

.= ((F | A) /. x) / ((F | A) /. (- x)) by A3, A8, PARTFUN2:17

.= ((F | A) . x) / ((F | A) /. (- x)) by A6, PARTFUN1:def 6

.= ((F | A) . x) / ((F | A) . (- x)) by A9, PARTFUN1:def 6

.= ((F | A) . x) / (- ((F | A) . x)) by A4, A6, A9, Def6

.= - (((F | A) . x) / ((F | A) . x)) by XCMPLX_1:188

.= - 1 by A2, A5, A7, XCMPLX_1:60 ;

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

(F . x) / (F . (- x)) = - 1 ) ) by A1; :: thesis: verum