let F, G be PartFunc of REAL,REAL; ( F is even & G is odd & (dom F) /\ (dom G) is symmetrical implies F (#) G is odd )
assume that
A1:
F is even
and
A2:
G is odd
and
A3:
(dom F) /\ (dom G) is symmetrical
; F (#) G is odd
A4:
(dom F) /\ (dom G) = dom (F (#) G)
by VALUED_1:def 4;
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
let x be
Real;
( 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)
;
(F (#) G) . (- x) = - ((F (#) G) . x)
(F (#) G) . (- x) =
(F . (- x)) * (G . (- x))
by A8, VALUED_1:def 4
.=
(F . x) * (G . (- x))
by A1, A6, A7, A8, Def3
.=
(F . x) * (- (G . x))
by A2, A5, A7, A8, Def6
.=
- ((F . x) * (G . x))
.=
- ((F (#) G) . x)
by A7, VALUED_1:def 4
;
hence
(F (#) G) . (- x) = - ((F (#) G) . x)
;
verum
end;
then
( F (#) G is with_symmetrical_domain & F (#) G is quasi_odd )
by A3, A4;
hence
F (#) G is odd
; verum