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

( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) ) )

let F be PartFunc of REAL,REAL; :: thesis: ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) ) )

A1: ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) implies F is_odd_on A )

(F . x) + (F . (- x)) = 0 ) ) )

(F . x) + (F . (- x)) = 0 ) ) ) by A1; :: thesis: verum

( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) ) )

let F be PartFunc of REAL,REAL; :: thesis: ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) ) )

A1: ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) implies F is_odd_on A )

proof

( F is_odd_on A implies ( A c= dom F & ( for x being Real st x in A holds
assume that

A2: A c= dom F and

A3: for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ; :: thesis: F is_odd_on A

A4: dom (F | A) = A by A2, RELAT_1:62;

A5: for x being Real st x in A holds

F . (- x) = - (F . x)

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

hence F is_odd_on A by A2; :: thesis: verum

end;A2: A c= dom F and

A3: for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ; :: thesis: F is_odd_on A

A4: dom (F | A) = A by A2, RELAT_1:62;

A5: for x being Real st x in A holds

F . (- x) = - (F . x)

proof

for x being Real st x in dom (F | A) & - x in dom (F | A) holds
let x be Real; :: thesis: ( x in A implies F . (- x) = - (F . x) )

assume x in A ; :: thesis: F . (- x) = - (F . x)

then (F . x) + (F . (- x)) = 0 by A3;

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

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

then (F . x) + (F . (- x)) = 0 by A3;

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

(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)

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 A2, A4, A7, PARTFUN2:17

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

.= - (F . x) by A5, A6

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

.= - ((F | A) /. x) by A2, 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)

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 A2, A4, A7, PARTFUN2:17

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

.= - (F . x) by A5, A6

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

.= - ((F | A) /. x) by A2, 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 A2; :: thesis: verum

(F . x) + (F . (- x)) = 0 ) ) )

proof

hence
( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds
assume A8:
F is_odd_on A
; :: thesis: ( A c= dom F & ( for x being Real st x in A holds

(F . x) + (F . (- x)) = 0 ) )

then A9: A c= dom F ;

A10: F | A is odd by A8;

for x being Real st x in A holds

(F . x) + (F . (- x)) = 0

(F . x) + (F . (- x)) = 0 ) ) by A8; :: thesis: verum

end;(F . x) + (F . (- x)) = 0 ) )

then A9: A c= dom F ;

A10: F | A is odd by A8;

for x being Real st x in A holds

(F . x) + (F . (- x)) = 0

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)) = 0 )

assume A11: x in A ; :: thesis: (F . x) + (F . (- x)) = 0

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

A13: - x in A by A11, Def1;

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

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

(F . x) + (F . (- x)) = (F /. x) + (F . (- x)) by A9, A11, PARTFUN1:def 6

.= (F /. x) + (F /. (- x)) by A9, A13, PARTFUN1:def 6

.= ((F | A) /. x) + (F /. (- x)) by A9, A11, PARTFUN2:17

.= ((F | A) /. x) + ((F | A) /. (- x)) by A9, A13, PARTFUN2:17

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

.= ((F | A) . x) + ((F | A) . (- x)) by A12, PARTFUN1:def 6

.= ((F | A) . x) + (- ((F | A) . x)) by A10, A12, A14, Def6

.= 0 ;

hence (F . x) + (F . (- x)) = 0 ; :: thesis: verum

end;assume A11: x in A ; :: thesis: (F . x) + (F . (- x)) = 0

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

A13: - x in A by A11, Def1;

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

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

(F . x) + (F . (- x)) = (F /. x) + (F . (- x)) by A9, A11, PARTFUN1:def 6

.= (F /. x) + (F /. (- x)) by A9, A13, PARTFUN1:def 6

.= ((F | A) /. x) + (F /. (- x)) by A9, A11, PARTFUN2:17

.= ((F | A) /. x) + ((F | A) /. (- x)) by A9, A13, PARTFUN2:17

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

.= ((F | A) . x) + ((F | A) . (- x)) by A12, PARTFUN1:def 6

.= ((F | A) . x) + (- ((F | A) . x)) by A10, A12, A14, Def6

.= 0 ;

hence (F . x) + (F . (- x)) = 0 ; :: thesis: verum

(F . x) + (F . (- x)) = 0 ) ) by A8; :: thesis: verum

(F . x) + (F . (- x)) = 0 ) ) ) by A1; :: thesis: verum