let A be symmetrical Subset of COMPLEX; :: thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds

F " is_odd_on A

let F be PartFunc of REAL,REAL; :: thesis: ( F is_odd_on A implies F " is_odd_on A )

assume A1: F is_odd_on A ; :: thesis: F " is_odd_on A

then A2: A c= dom F ;

then A3: A c= dom (F ") by VALUED_1:def 7;

then A4: dom ((F ") | A) = A by RELAT_1:62;

A5: F | A is odd by A1;

for x being Real st x in dom ((F ") | A) & - x in dom ((F ") | A) holds

((F ") | A) . (- x) = - (((F ") | A) . x)

hence F " is_odd_on A by A3; :: thesis: verum

F " is_odd_on A

let F be PartFunc of REAL,REAL; :: thesis: ( F is_odd_on A implies F " is_odd_on A )

assume A1: F is_odd_on A ; :: thesis: F " is_odd_on A

then A2: A c= dom F ;

then A3: A c= dom (F ") by VALUED_1:def 7;

then A4: dom ((F ") | A) = A by RELAT_1:62;

A5: F | A is odd by A1;

for x being Real st x in dom ((F ") | A) & - x in dom ((F ") | A) holds

((F ") | A) . (- x) = - (((F ") | A) . x)

proof

then
( (F ") | A is with_symmetrical_domain & (F ") | A is quasi_odd )
by A4;
let x be Real; :: thesis: ( x in dom ((F ") | A) & - x in dom ((F ") | A) implies ((F ") | A) . (- x) = - (((F ") | A) . x) )

assume that

A6: x in dom ((F ") | A) and

A7: - x in dom ((F ") | A) ; :: thesis: ((F ") | A) . (- x) = - (((F ") | A) . x)

A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;

A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;

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

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

.= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17

.= (F ") . (- x) by A3, A7, PARTFUN1:def 6

.= (F . (- x)) " by A3, A7, VALUED_1:def 7

.= (F /. (- x)) " by A2, A7, PARTFUN1:def 6

.= ((F | A) /. (- x)) " by A2, A4, A7, PARTFUN2:17

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

.= (- ((F | A) . x)) " by A5, A8, A9, Def6

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

.= (- (F /. x)) " by A2, A4, A6, PARTFUN2:17

.= (- (F . x)) " by A2, A6, PARTFUN1:def 6

.= - ((F . x) ") by XCMPLX_1:222

.= - ((F ") . x) by A3, A6, VALUED_1:def 7

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

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

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

hence ((F ") | A) . (- x) = - (((F ") | A) . x) ; :: thesis: verum

end;assume that

A6: x in dom ((F ") | A) and

A7: - x in dom ((F ") | A) ; :: thesis: ((F ") | A) . (- x) = - (((F ") | A) . x)

A8: x in dom (F | A) by A2, A4, A6, RELAT_1:62;

A9: - x in dom (F | A) by A2, A4, A7, RELAT_1:62;

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

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

.= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17

.= (F ") . (- x) by A3, A7, PARTFUN1:def 6

.= (F . (- x)) " by A3, A7, VALUED_1:def 7

.= (F /. (- x)) " by A2, A7, PARTFUN1:def 6

.= ((F | A) /. (- x)) " by A2, A4, A7, PARTFUN2:17

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

.= (- ((F | A) . x)) " by A5, A8, A9, Def6

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

.= (- (F /. x)) " by A2, A4, A6, PARTFUN2:17

.= (- (F . x)) " by A2, A6, PARTFUN1:def 6

.= - ((F . x) ") by XCMPLX_1:222

.= - ((F ") . x) by A3, A6, VALUED_1:def 7

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

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

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

hence ((F ") | A) . (- x) = - (((F ") | A) . x) ; :: thesis: verum

hence F " is_odd_on A by A3; :: thesis: verum