let A be symmetrical Subset of COMPLEX; for F being PartFunc of REAL,REAL st F is_even_on A holds
|.F.| is_even_on A
let F be PartFunc of REAL,REAL; ( F is_even_on A implies |.F.| is_even_on A )
assume A1:
F is_even_on A
; |.F.| is_even_on A
then A2:
A c= dom F
;
then A3:
A c= dom |.F.|
by VALUED_1:def 11;
then A4:
dom (|.F.| | A) = A
by RELAT_1:62;
A5:
F | A is even
by A1;
for x being Real st x in dom (|.F.| | A) & - x in dom (|.F.| | A) holds
(|.F.| | A) . (- x) = (|.F.| | A) . x
proof
let x be
Real;
( 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)
;
(|.F.| | A) . (- x) = (|.F.| | A) . x
A8:
x in dom (F | A)
by A2, A4, A6, RELAT_1:62;
A9:
- x in dom (F | A)
by A2, A4, A7, RELAT_1:62;
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 A3, A4, A7, PARTFUN2:17
.=
|.F.| . (- x)
by A3, A7, PARTFUN1:def 6
.=
|.(F . (- x)).|
by A3, A7, VALUED_1:def 11
.=
|.(F /. (- x)).|
by A2, A7, PARTFUN1:def 6
.=
|.((F | A) /. (- x)).|
by A2, A4, A7, PARTFUN2:17
.=
|.((F | A) . (- x)).|
by A9, PARTFUN1:def 6
.=
|.((F | A) . x).|
by A5, A8, A9, Def3
.=
|.((F | A) /. x).|
by A8, PARTFUN1:def 6
.=
|.(F /. x).|
by A2, A4, A6, PARTFUN2:17
.=
|.(F . x).|
by A2, A6, PARTFUN1:def 6
.=
|.F.| . x
by A3, A6, VALUED_1:def 11
.=
|.F.| /. x
by A3, A6, PARTFUN1:def 6
.=
(|.F.| | A) /. x
by A3, A4, A6, PARTFUN2:17
.=
(|.F.| | A) . x
by A6, PARTFUN1:def 6
;
hence
(|.F.| | A) . (- x) = (|.F.| | A) . x
;
verum
end;
then
( |.F.| | A is with_symmetrical_domain & |.F.| | A is quasi_even )
by A4;
hence
|.F.| is_even_on A
by A3; verum