let F, G be PartFunc of REAL,REAL; :: thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F - G is odd )

assume that

A1: F is odd and

A2: G is odd and

A3: (dom F) /\ (dom G) is symmetrical ; :: thesis: F - G is odd

A4: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;

then A5: dom (F - G) c= dom G by XBOOLE_1:17;

A6: dom (F - G) c= dom F by A4, XBOOLE_1:17;

for x being Real st x in dom (F - G) & - x in dom (F - G) holds

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

hence F - G is odd ; :: thesis: verum

assume that

A1: F is odd and

A2: G is odd and

A3: (dom F) /\ (dom G) is symmetrical ; :: thesis: F - G is odd

A4: (dom F) /\ (dom G) = dom (F - G) by VALUED_1:12;

then A5: dom (F - G) c= dom G by XBOOLE_1:17;

A6: dom (F - G) c= dom F by A4, XBOOLE_1:17;

for x being Real st x in dom (F - G) & - x in dom (F - G) holds

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

proof

then
( F - G is with_symmetrical_domain & F - G is quasi_odd )
by A3, A4;
let x be Real; :: thesis: ( x in dom (F - G) & - x in dom (F - G) implies (F - G) . (- x) = - ((F - G) . x) )

assume that

A7: x in dom (F - G) and

A8: - x in dom (F - G) ; :: thesis: (F - G) . (- x) = - ((F - G) . x)

(F - G) . (- x) = (F . (- x)) - (G . (- x)) by A8, VALUED_1:13

.= (- (F . x)) - (G . (- x)) by A1, A6, A7, A8, Def6

.= (- (F . x)) - (- (G . x)) by A2, A5, A7, A8, Def6

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

.= - ((F - G) . x) by A7, VALUED_1:13 ;

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

end;assume that

A7: x in dom (F - G) and

A8: - x in dom (F - G) ; :: thesis: (F - G) . (- x) = - ((F - G) . x)

(F - G) . (- x) = (F . (- x)) - (G . (- x)) by A8, VALUED_1:13

.= (- (F . x)) - (G . (- x)) by A1, A6, A7, A8, Def6

.= (- (F . x)) - (- (G . x)) by A2, A5, A7, A8, Def6

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

.= - ((F - G) . x) by A7, VALUED_1:13 ;

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

hence F - G is odd ; :: thesis: verum