let A be symmetrical Subset of COMPLEX ; :: thesis: for F, G being PartFunc of REAL ,REAL st F is_odd_on A & G is_even_on A holds
F /" G is_odd_on A
let F, G be PartFunc of REAL ,REAL ; :: thesis: ( F is_odd_on A & G is_even_on A implies F /" G is_odd_on A )
assume that
A1: F is_odd_on A and
A2: G is_even_on A ; :: thesis: F /" G is_odd_on A
B1: ( A c= dom F & F | A is odd ) by Def8, A1;
B2: ( A c= dom G & G | A is even ) by Def5, A2;
B3: A c= (dom F) /\ (dom G) by XBOOLE_1:19, B1, B2;
A7: (dom F) /\ (dom G) = dom (F /" G) by VALUED_1:16;
A8: dom ((F /" G) | A) = A by RELAT_1:91, A7, XBOOLE_1:19, B1, B2;
for x being Real st x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) holds
((F /" G) | A) . (- x) = - (((F /" G) | A) . x)

proof

let x be Real; :: thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) )
assume A9: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) ) ; :: thesis: ((F /" G) | A) . (- x) = - (((F /" G) | A) . x)
then A10: ( x in dom (F | A) & - x in dom (F | A) & x in dom (G | A) & - x in dom (G | A) ) by RELAT_1:91, B1, B2, A8;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by PARTFUN1:def 8, A9
.= (F /" G) /. (- x) by PARTFUN2:35, A9, A8, B3, A7
.= (F /" G) . (- x) by PARTFUN1:def 8, A9, A8, B3, A7
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by PARTFUN1:def 8, B1, A9, A8
.= (F /. (- x)) / (G /. (- x)) by PARTFUN1:def 8, B2, A9, A8
.= ((F | A) /. (- x)) / (G /. (- x)) by PARTFUN2:35, A9, B1, A8
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by PARTFUN2:35, A9, B2, A8
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by PARTFUN1:def 8, A10
.= ((F | A) . (- x)) / ((G | A) . (- x)) by PARTFUN1:def 8, A10
.= (- ((F | A) . x)) / ((G | A) . (- x)) by B1, Def6, A10
.= (- ((F | A) . x)) / ((G | A) . x) by B2, Def3, A10
.= - (((F | A) . x) / ((G | A) . x))
.= - (((F | A) /. x) / ((G | A) . x)) by PARTFUN1:def 8, A10
.= - (((F | A) /. x) / ((G | A) /. x)) by PARTFUN1:def 8, A10
.= - ((F /. x) / ((G | A) /. x)) by PARTFUN2:35, B1, A9, A8
.= - ((F /. x) / (G /. x)) by PARTFUN2:35, B2, A9, A8
.= - ((F . x) / (G /. x)) by PARTFUN1:def 8, B1, A9, A8
.= - ((F . x) / (G . x)) by PARTFUN1:def 8, B2, A9, A8
.= - ((F /" G) . x) by VALUED_1:17
.= - ((F /" G) /. x) by PARTFUN1:def 8, A9, A8, B3, A7
.= - (((F /" G) | A) /. x) by PARTFUN2:35, A9, A8, B3, A7
.= - (((F /" G) | A) . x) by PARTFUN1:def 8, A9 ;
hence ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ; :: thesis: verum

end;

then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_odd ) by Def6, A8, Def2;
hence F /" G is_odd_on A by A7, B3, Def8; :: thesis: verum