let A be symmetrical Subset of COMPLEX; for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds
F - G is_even_on A
let F, G be PartFunc of REAL,REAL; ( F is_even_on A & G is_even_on A implies F - G is_even_on A )
assume that
A1:
F is_even_on A
and
A2:
G is_even_on A
; F - G is_even_on A
A3:
A c= dom G
by A2;
A4:
G | A is even
by A2;
A5:
A c= dom F
by A1;
then A6:
A c= (dom F) /\ (dom G)
by A3, XBOOLE_1:19;
A7:
(dom F) /\ (dom G) = dom (F - G)
by VALUED_1:12;
then A8:
dom ((F - G) | A) = A
by A5, A3, RELAT_1:62, XBOOLE_1:19;
A9:
F | A is even
by A1;
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;
( x in dom ((F - G) | A) & - x in dom ((F - G) | A) implies ((F - G) | A) . (- x) = ((F - G) | A) . x )
assume that A10:
x in dom ((F - G) | A)
and A11:
- x in dom ((F - G) | A)
;
((F - G) | A) . (- x) = ((F - G) | A) . x
A12:
x in dom (F | A)
by A5, A8, A10, RELAT_1:62;
A13:
x in dom (G | A)
by A3, A8, A10, RELAT_1:62;
A14:
- x in dom (F | A)
by A5, A8, A11, RELAT_1:62;
A15:
- x in dom (G | A)
by A3, A8, A11, RELAT_1:62;
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
((F - G) | A) . (- x) =
((F - G) | A) /. (- x)
by A11, PARTFUN1:def 6
.=
(F - G) /. (- x)
by A6, A7, A8, A11, PARTFUN2:17
.=
(F - G) . (- x)
by A6, A7, A11, PARTFUN1:def 6
.=
(F . (- x)) - (G . (- x))
by A6, A7, A11, VALUED_1:13
.=
(F /. (- x)) - (G . (- x))
by A5, A11, PARTFUN1:def 6
.=
(F /. (- x)) - (G /. (- x))
by A3, A11, PARTFUN1:def 6
.=
((F | A) /. (- x)) - (G /. (- x))
by A5, A8, A11, PARTFUN2:17
.=
((F | A) /. (- x)) - ((G | A) /. (- x))
by A3, A8, A11, PARTFUN2:17
.=
((F | A) . (- x)) - ((G | A) /. (- x))
by A14, PARTFUN1:def 6
.=
((F | A) . (- x)) - ((G | A) . (- x))
by A15, PARTFUN1:def 6
.=
((F | A) . x) - ((G | A) . (- x))
by A9, A12, A14, Def3
.=
((F | A) . x) - ((G | A) . x)
by A4, A13, A15, Def3
.=
((F | A) /. x) - ((G | A) . x)
by A12, PARTFUN1:def 6
.=
((F | A) /. x) - ((G | A) /. x)
by A13, PARTFUN1:def 6
.=
(F /. x) - ((G | A) /. x)
by A5, A8, A10, PARTFUN2:17
.=
(F /. x) - (G /. x)
by A3, A8, A10, PARTFUN2:17
.=
(F . x) - (G /. x)
by A5, A10, PARTFUN1:def 6
.=
(F . x) - (G . x)
by A3, A10, PARTFUN1:def 6
.=
(F - G) . x
by A6, A7, A10, VALUED_1:13
.=
(F - G) /. x
by A6, A7, A10, PARTFUN1:def 6
.=
((F - G) | A) /. x
by A6, A7, A8, A10, PARTFUN2:17
.=
((F - G) | A) . x
by A10, PARTFUN1:def 6
;
hence
((F - G) | A) . (- x) = ((F - G) | A) . x
;
verum
end;
then
( (F - G) | A is with_symmetrical_domain & (F - G) | A is quasi_even )
by A8;
hence
F - G is_even_on A
by A6, A7; verum